perm filename PROVE1.NEW[1,JRA]2 blob
sn#026654 filedate 1973-02-28 generic text, type T, neo UTF8
00100
00200
00300 (DEFPROP NEWPROOF
00400 (NIL NEWPROOF
00500 ALLPOS
00600 ALLNEG
00700 ANCESTOR
00800 SEARCH1
00900 CONST
01000 HERE
01100 VAR
01200 ISCLS
01300 ISCL
01400 ISLIT
01500 ISTRM
01600 MKWRD
01700 NEG
01800 NEGBIT
01900 POS
02000 POSBIT
02100 SEARCH
02200 NUM
02300 NEGL
02400 APPENDIT
02500 ANDOR
02600 ASSOC1
02700 ATTEMPT
02800 AUTO
02900 BAKSUB
03000 BOOKEEP
03100 BUILTED
03200 BUILTED1
03300 BUILTCH
03400 BUILTCH1
03500 CHOICE
03600 CHOICE1
03700 CLAUSES
03800 CLAUSES2
03900 CLAUSES1
04000 CNF
04100 CNF1
04200 CNF2
04300 CNF3
04400 CNVT
04500 CNVT2
04600 CNVT3
04700 COPY
04800 COPYDELETED
04900 *CL
05000 DEMOD
05100 DEM
05200 DEPTH
05300 DEPTH1
05400 DEL
05500 DOML
05600 DOMC
05700 DOWN
05800 EDIT
05900 ERPRINT
06000 ERPRIN1
06100 EXPUNGE
06200 FINI
06300 FIXNEG
06400 FIXQFF
06500 FIXQFF1
06600 GENSKOLEM
06700 GETNAME
06800 GETTERMS
06900 GETVARS
07000 GOLIST
07100 INCLAUSES
07200 INITIAL
07300 INITIALAX
07400 INITIALAX1
07500 MAKVAR
07600 MAKOVAR
07700 MAPIT
07800 MATCHER
07900 MATCH1
08000 MATCHTR
08100 MATCHPN
08200 MATMLT
08300 MATMLT*
08400 MAX
08500 MEMC
08600 MIN1
08700 MINIMIZE
08800 MIN
08900 MKSYM
09000 MODEL
09100 NCONC1
09200 NEGATE
09300 NEGSGN
09400 NOSYM
09500 OCR
09600 OCR1
09700 ONEGSGN
09800 *NOPOINT
09900 OCCUR
10000 ORDER
10100 ORDEREQUAL
10200 PARMOD
10300 PARMOD1
10400 POTZ
10500 PRECNF
10600 PROOF1
10700 PROVE
10800 PRPAR
10900 PRFPRINT
11000 PRFPR1
11100 PROOF
11200 PTRS
11300 PUNIFY
11400 QUERY
11500 REAL-LNGTH
11600 REDUCER
12000 RESOLVE
12100 RESOLVE1
12300 RESET
12400 RESET1
12700 SET1
12800 SET2
12900 SET3
13000 SETUP
13100 SEARCH2
13200 S2
13300 SETQUERY
13400 SETQUERY1
13500 SETQUERY2
13600 SETSUP
13700 SUBS3TA
13800 SUBS3T**
13900 SUB*
14000 SUBSKOL
14100 SUPPORT
14200 SUBSUME1
14300 SUBS2T
14400 SUBS3T
14500 SUBSUME
14600 SUBSUME*
14700 SUBST1
14800 TCOPY
14900 TERMS
15000 TERMS1
15100 TERMS2
15200 TIMEIT
15300 TREE
15400 TREEDEP
15500 TRY
15600 TRY1
15700 TRYIT
15800 TRAVERSE
15900 UNIT
16000 UNITS
16100 UNITRES
16200 UNITREDUCT
16300 UNITPN
16400 UNIFY
16500 UNI
16600 UNION
16700 UNWIND
16800 UPDATE
16900 UPGETL
17000 UPGETL1
17100 UPGETNU
17200 UPDATESTATE
17300 UPIT
17400 UPIT1
17500 UP1A
17600 UP1B
17700 VARIT
17800 VINE
17900 <)
18000 VALUE)
18100
18200 (DEFPROP ALLPOS
18300 (LAMBDA (C) (LIST (QUOTE NULL) (LIST (QUOTE CADAR) (CADR C))))
18400 MACRO)
18500
18600 (DEFPROP ALLNEG
18700 (LAMBDA (C) (LIST (QUOTE EQ) (LIST (QUOTE CADAR) (CADR C)) (LIST (QUOTE CDR) (CADR C))))
18800 MACRO)
18900
19000 (DEFPROP ANCESTOR
19100 (LAMBDA (X) (LIST (QUOTE CDDDAR) (CADR X)))
19200 MACRO)
19300
19400 (DEFPROP SEARCH1
19500 (LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) NIL))
19600 MACRO)
19700
19800 (DEFPROP CONST
19900 (LAMBDA (X) (LIST (QUOTE NULL) (LIST (QUOTE CDR) (CADR X))))
20000 MACRO)
20100
20200 (DEFPROP HERE
20300 (LAMBDA (X) (LIST (QUOTE CAAR) (CADR X)))
20400 MACRO)
20500
20600 (DEFPROP VAR
20700 (LAMBDA (L) (LIST (QUOTE NUMBERP) (CADR L)))
20800 MACRO)
20900
21000 (DEFPROP ISCLS
21100 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 1))
21200 MACRO)
21300
21400 (DEFPROP ISCL
21500 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 2))
21600 MACRO)
21700
21800 (DEFPROP ISLIT
21900 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 3))
22000 MACRO)
22100
22200 (DEFPROP ISTRM
22300 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 4))
22400 MACRO)
22500
22600 (DEFPROP MKWRD
22700 (LAMBDA (L) (LIST (QUOTE CDDAR) (CADR L)))
22800 MACRO)
22900
23000 (DEFPROP NEG
23100 (LAMBDA (X) (LIST (QUOTE EQ) (QUOTE ESCAPE) (LIST (QUOTE CAR) (CADR X))))
23200 MACRO)
23300
23400 (DEFPROP NEGBIT
23500 (LAMBDA (X) (LIST (QUOTE CDDAAR) (CADR X)))
23600 MACRO)
23700
23800 (DEFPROP POS
23900 (LAMBDA (X) (LIST (QUOTE NOT) (LIST (QUOTE NEG) (CADR X))))
24000 MACRO)
24100
24200 (DEFPROP POSBIT
24300 (LAMBDA (X) (LIST (QUOTE CADAAR) (CADR X)))
24400 MACRO)
24500
24600 (DEFPROP SEARCH
24700 (LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) (CADR X)))
24800 MACRO)
24900
25000 (DEFPROP NUM
25100 (LAMBDA (C) (LIST (QUOTE CAAAR) (CADR C)))
25200 MACRO)
25300
25400 (DEFPROP NEGL
25500 (LAMBDA (C) (LIST (QUOTE CADAR) (CADR C)))
25600 MACRO)
25700
25800 (DEFPROP APPENDIT
25900 (LAMBDA(X Y)
26000 (PROG NIL (COND (USINGFL (SETQ USING (CONS N2 (APPEND (REVERSE Y) USING))))) (RETURN (APPEND X Y))))
26100 EXPR)
26200
26300 (DEFPROP ANDOR
26400 (LAMBDA(C UNL EXL PF)
26500 (PROG (Z1 Z2)
26600 (SETQ Z1 (CADR C))
26700 (SETQ Z2 (CADDR C))
26800 (COND
26900 ((OR (AND (EQ (CAR C) (QUOTE AND)) PF) (AND (EQ (CAR C) (QUOTE OR)) (NOT PF)))
27000 (RETURN (LIST (QUOTE AND) Z1 Z2)))
27100 ((EQ (CAR Z1) (QUOTE AND))
27200 (RETURN
27300 (LIST (QUOTE AND)
27400 (CNF1 (LIST (QUOTE OR) (CADR Z1) Z2) UNL EXL T)
27500 (CNF1 (LIST (QUOTE OR) (CADDR Z1) (COPY Z2)) UNL EXL T))))
27600 ((EQ (CAR Z2) (QUOTE AND))
27700 (RETURN
27800 (LIST (QUOTE AND)
27900 (CNF1 (LIST (QUOTE OR) (CADR Z2) (COPY Z1)) UNL EXL T)
28000 (CNF1 (LIST (QUOTE OR) (CADDR Z2) Z1) UNL EXL T))))
28100 (T (RETURN (LIST (QUOTE OR) Z1 Z2))))))
28200 EXPR)
28300
28400 (DEFPROP ASSOC1
28500 (LAMBDA (X L) (COND ((NULL L) NIL) ((EQ (CDR X) (CDAAR L)) (CAR L)) (T (ASSOC1 X (CDR L)))))
28600 EXPR)
28700
28800 (DEFPROP ATTEMPT
28900 (LAMBDA(Z S C)
29000 (PROG (NEWNAME SUPPORT
29100 EDITSTRAT
29200 LCL
29300 LVL
29400 CNT
29500 LSTCLS
29600 LLST
29700 Z1
29800 MERGE
29900 ORDER
30000 DEBUG
30100 DEPTH
30200 LENGTH
30300 ANCESTRY
30400 STRATEGY
30500 STRAT
30600 PMODEL
30700 NMODEL
30800 PFLG
30900 PDEPTH
31000 DLIST
31100 XYZ
31200 XYZ1
31300 COND
31400 UNAXP
31500 UNAXN
31600 SAT
31700 EE
31800 EE1
31900 CLAUSES
32000 SUBCLAUSES
32100 COUNT)
32200 (SETQ TBL (SET1 (APPEND PREFN INFN)))
32300 (SET3 Z)
32400 (SETQ Z (MINIMIZE Z))
32500 (SETQ NEWNAME (INITIAL Z))
32600 (SETQ CLAUSES Z)
32700 (UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
32800 (SETQ COND C)
32900 (SETQ LVL 1)
33000 (SETQ COUNT 0)
33100 (SETQ Z (UNITPN Z))
33200 (SETQ UNAXP (CAR Z))
33300 (SETQ UNAXN (CDR Z))
33400 (COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
33500 (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
33600 (T (SETQ SUBCLAUSES CLAUSES)))
33700 (SETQ LCL (LAST CLAUSES))
33800 (SETQ LSTCLS LCL)
33900 (SETQ XYZ (SETQ EE CLAUSES))
34000 (SETQ EE1 (LAST CLAUSES))
34100 BB (SETQ LLST (CONS (CAR XYZ) LLST))
34200 (SETQ XYZ (CDR XYZ))
34300 (COND (XYZ (GO BB)))
34400 (SETQ Z1 (ERRSET (TRYIT)))
34500 (COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
34600 ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
34700 (EVAL
34800 (LIST (QUOTE OUTC)
34900 (LIST (QUOTE OUTPUT)
35000 (QUOTE PRF)
35100 (QUOTE DSK:)
35200 (CONS (READLIST
35300 (CONS (QUOTE N)
35400 (CONS (SETQ PRNO (ADD1 PRNO))
35500 FILENAM)))
35600 (QUOTE PRF)))
35700 NIL)))
35800 (QUERY)
35900 (PROOF LHP RHP)
36000 (OUTC Z T)
36100 (RETURN Z1))
36200 (T (RETURN Z1)))))
36300 EXPR)
36400
36500 (DEFPROP AUTO
36600 (LAMBDA(XX)
36700 (PROG (X1 Z2 D M STRATEGY SUPPORT EDITSTRAT MERGE ORDER DEBUG ANCESTRY PMODEL NMODEL PFLG PDEPTH DLIST)
36800 (COND (EQUAL (SETQ PFLG NIL)) (T (SETQ PFLG NIL)))
36900 (SETQ PDEPTH 3)
37000 (SETQ DDEPTH 4)
37700 (SETQ X1 XX)
37800 (SETQ M (SETQ D 0))
37900 A (SETQ M (MAX M (LENGTH (CDAR X1))))
38000 (SETQ D (MAX D (DEPTH (CDAR X1))))
38100 (SETQ Z2 (CAR X1))
38200 (COND
38300 ((AND (EQ (LENGTH (CDR Z2)) 1) (EQ (CAADR Z2) EQUAL) (NOT (EQ (CADADR Z2) (CAR (CDDADR Z2)))))
38400 (SETQ DLIST (CONS (CONS (CONS (CAAAR Z2) (CDAR Z2)) (CDR Z2)) DLIST))))
38500 (SETQ X1 (CDR X1))
38600 (COND ((CDR X1) (GO A)))
38700 (SETQ Z2 (ASSOC (QUOTE THEOREM) NEWNAME))
38800 (COND ((NULL Z2) (GO C)) (T (SETQ Z2 (CDR Z2))))
38900 B (COND (Z2 (SETQ SUPPORT (CONS (CDAR Z2) SUPPORT)) (SETQ Z2 (CDR Z2)) (GO B)))
39000 C (COND ((NULL LENGTH) (SETQ LENGTH (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2)))
39100 ((ZEROP ITER) (SETQ LENGTH (ADD1 LENGTH))))
39200 (COND ((NOT (GREATERP LENGTH 0)) (SETQ LENGTH 1)))
39300 (COND ((NULL DEPTH) (SETQ DEPTH (ADD1 D))) ((NOT (ZEROP ITER)) (SETQ DEPTH (ADD1 DEPTH))))
39400 (COND ((ZEROP ITER) (SETQ ITER 1)) (T (SETQ ITER 0)))
39500 (COND (SUPPORT (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (OR(SUPPORT C2)(SUPPORT C1)))))
39550 (SETQ SAVESTR @(AND ANCESTRY(SUPPORT THEOREM))))
39575 (T(SETQ SAVESTR @ANCESTRY)))
39600 (SETQ ANCESTRY T)
39700 (SETQ EDITSTRAT
39800 (QUOTE (LAMBDA (C) (OR (GREATERP (LENGTH (CDR C)) LENGTH) (GREATERP (DEPTH (CDR C)) DEPTH)))))
39900 (SETQ DEBUG T)
40000 (COND (DLIST (SET3 DLIST)))
40050 (COND(EQUAL(SETQ SAVESTR(CONS @AND(CONS SAVESTR(LIST(LIST @EQUALITY EQUAL PDEPTH)))))))
40100 (RETURN
40200 (LIST STRATEGY
40300 SUPPORT
40400 EDITSTRAT
40500 MERGE
40600 ORDER
40700 DEBUG
40800 DEPTH
40900 LENGTH
41000 ANCESTRY
41100 PMODEL
41200 NMODEL
41300 PFLG
41400 EQUAL
41500 PDEPTH
41600 DLIST))))
41700 EXPR)
41800
41900 (DEFPROP AUTO
42000 (NIL . T)
42100 VALUE)
42200
42300 (DEFPROP BAKSUB
42400 (LAMBDA(L R)
42500 (PROG (Z U1 U4)
42600 (SETQ Z L)
42700 ED4 (COND ((NOT Z) (RETURN NIL)) ((OR (NOT (HERE (CAR Z))) (ATOM (CDR (ANCESTOR (CAR Z))))) (GO ED6A)))
42800 (SETQ U1 R)
42900 ED3 (SETQ U4 (CAR Z))
43000 ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
43100 ED6 (SETQ U1 (CDR U1))
43200 (COND (U1 (GO ED1)))
43300 ED6A (SETQ Z (CDR Z))
43400 (GO ED4)
43500 ED2 (DEL U4)
43600 (GO ED4)))
43700 EXPR)
43800
43900 (DEFPROP BOOKEEP
44000 (LAMBDA(L M N)
44100 (PROG (U)
44200 B1 (SETQ U M)
44300 B3 (RPLACD (CDAAR U) (CONS 0 N))
44400 (SETQ U (CDR U))
44500 (COND ((NULL U) (RETURN (NCONC L M))))
44600 (GO B3)))
44700 EXPR)
44800
44900 (DEFPROP BUILTED
45000 (LAMBDA (X) (LIST (QUOTE LAMBDA) (QUOTE (C)) (BUILTED1 X)))
45100 EXPR)
45200
45300 (DEFPROP BUILTED1
45400 (LAMBDA(X)
45500 (COND ((ATOM X) X)
45600 ((ATOM (CAR X)) (CONS (CAR X) (BUILTED1 (CDR X))))
45700 ((EQ (CAAR X) (QUOTE DEMOD)) (SETQ DDEPTH (CADDAR X)) (SETQ DLIST (*CL (CADAR X))) (BUILTED1 (CDR X)))
45800 (T (CONS (BUILTED1 (CAR X)) (BUILTED1 (CDR X))))))
45900 EXPR)
46000
46100 (DEFPROP BUILTCH
46200 (LAMBDA(X)
46300 (PROG (Z)
46400 (SETQ Z (BUILTCH1 X))
46500 (RETURN
46600 (COND ((OR (ATOM Z) (EQUAL Z (QUOTE (AND))) (EQUAL X (QUOTE (OR)))) NIL)
46700 (T (LIST (QUOTE LAMBDA) (QUOTE (C1 C2)) Z))))))
46800 EXPR)
46900
47000 (DEFPROP BUILTCH1
47100 (LAMBDA(X)
47200 (COND ((ATOM X)
47300 (COND ((EQ X (QUOTE ANCESTRY)) (SETQ ANCESTRY T) NIL)
47400 ((EQ X (QUOTE NONE)) NIL)
47500 ((MEMQ X (QUOTE (VINE ALLPOS ALLNEG UNIT)))
47600 (LIST (QUOTE OR) (LIST X (QUOTE C1)) (LIST X (QUOTE C2))))
47700 (T X)))
47800 ((EQ (CAR X) (QUOTE SUPPORT)) (SETSUP (CDR X)) (QUOTE (OR(SUPPORT C2)(SUPPORT C1))))
47900 ((EQ (CAR X) (QUOTE MODEL)) (SETQ PMODEL (CADR X))
48000 (SETQ NMODEL (CADDR X))
48100 (QUOTE (OR (NOT (MODEL C1)) (NOT (MODEL C2)))))
48200 ((EQ (CAR X) (QUOTE DEFMODEL))
48300 (LIST (QUOTE OR)
48400 (LIST (QUOTE NOT) (LIST (CDR X) (QUOTE C1)))
48500 (LIST (QUOTE NOT) (LIST (CDR X) (QUOTE C2)))))
48600 ((EQ (CAR X) (QUOTE ANCESTRY)) (SETQ ANCESTRY T) (BUILTCH1 (CDR X)))
48700 ((ATOM (CAR X)) (CONS (CAR X) (BUILTCH1 (CDR X))))
48800 ((EQ (CAAR X) (QUOTE EQUALITY)) (SETQ PFLG NIL)
48900 (SETQ EQUAL (CADAR X))
49000 (SETQ PDEPTH (CADDAR X))
49100 (BUILTCH1 (CDR X)))
49200 (T (CONS (BUILTCH1 (CAR X)) (BUILTCH1 (CDR X))))))
49300 EXPR)
49400
49500 (DEFPROP CHOICE
49600 (LAMBDA(X)
49700 (PROG (Z Z1 Z2)
49800 (COND ((NOT (HERE X)) (RETURN NIL)) (ANCESTRY (SETQ Z (CHOICE1 X LLST))) (T (SETQ Z CLAUSES)))
49900 A (SETQ Z1 (CAR Z))
50000 (COND
50100 ((OR (NOT (HERE Z1))
50200 (AND PFLG (ALLPOS X) (ALLPOS Z1))
50300 (AND (ALLNEG Z1) (ALLNEG X))
50400 (AND STRATEGY (NOT (STRATEGY X Z1))))
50500 NIL)
50600 (T (SETQ Z2 (NCONC Z2 (LIST Z1)))))
50700 (SETQ Z (CDR Z))
50800 (COND ((OR (EQ Z X) (NULL Z)) (RETURN Z2)))
50900 (GO A)))
51000 EXPR)
51100
51200 (DEFPROP CHOICE1
51300 (LAMBDA (L LL) (COND ((ATOM (CDR (ANCESTOR L))) LL) (T (NCONC (CDR (TRAVERSE L)) LL))))
51400 EXPR)
51500
51600 (DEFPROP CLAUSES
51700 (LAMBDA (U) (PROG (DEBUG) (SETQ DEBUG T) (RETURN (CLAUSES1 U 1))))
51800 EXPR)
51900
52000 (DEFPROP CLAUSES2
52100 (LAMBDA (U) (CLAUSES1 U CNT))
52200 EXPR)
52300
52400 (DEFPROP CLAUSES1
52500 (LAMBDA(U N)
52600 (PROG NIL
52700 (COND ((NOT DEBUG) (RETURN NIL)))
52800 (COND ((NULL (CAR U)) (RETURN NIL)))
52900 CL1 (COND ((NULL U) (RETURN NIL)))
53000 (UP1A (CAR U) N)
53100 CL2 (SETQ U (CDR U))
53200 (SETQ N (ADD1 N))
53300 (GO CL1)))
53400 EXPR)
53500
53600 (DEFPROP CNF
53700 (LAMBDA(C1)
53800 (PROG (C)
53900 (SETQ C (PRECNF C1))
54000 (RETURN (CNF2 (COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) NIL NIL NIL)) (T (CNF1 C NIL NIL T)))))))
54100 EXPR)
54200
54300 (DEFPROP CNF1
54400 (LAMBDA(C UNL EXL PF)
54500 (COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) UNL EXL (COND (PF NIL) (T T))))
54600 ((MEMQ (CAR C) (QUOTE (AND OR)))
54700 (ANDOR (LIST (CAR C) (CNF1 (CADR C) UNL EXL PF) (CNF1 (CADDR C) UNL EXL PF)) UNL EXL PF))
54800 ((OR (AND (EQ (CAR C) (QUOTE FA)) PF) (AND (EQ (CAR C) (QUOTE TE)) (NOT PF)))
54900 (CNF1 (CADDR C) (APPEND (CADR C) UNL) EXL PF))
55000 ((OR (EQ (CAR C) (QUOTE FA)) (EQ (CAR C) (QUOTE TE)))
55100 (CNF1 (CADDR C) UNL (APPEND (GENSKOLEM (CADR C) UNL) EXL) PF))
55200 (PF (SUBSKOL C EXL))
55300 (T (CONS ESCAPE (SUBSKOL C EXL)))))
55400 EXPR)
55500
55600 (DEFPROP CNF2
55700 (LAMBDA(C)
55800 (COND ((EQ (CAR C) (QUOTE AND)) (APPEND (CNF2 (CADR C)) (CNF2 (CADDR C))))
55900 ((EQ (CAR C) (QUOTE OR)) (LIST (CNF3 C)))
56000 (T (LIST (LIST C)))))
56100 EXPR)
56200
56300 (DEFPROP CNF3
56400 (LAMBDA (C) (COND ((NOT (EQ (CAR C) (QUOTE OR))) (LIST C)) (T (APPEND (CNF3 (CADR C)) (CNF3 (CADDR C))))))
56500 EXPR)
56600
56700 (DEFPROP CNVT
56800 (LAMBDA(Z)
56900 (PROG (ZP ZN VARL VARNO)
57000 (SETQ VARNO 0)
57100 (COND
57200 ((EQ (LENGTH Z) 1)
57300 (RETURN (COND ((EQ (CAAR Z) ESCAPE) (LIST (QUOTE NOT) (CNVT2 (CDAR Z)))) (T (CNVT2 (CAR Z)))))))
57400 A1 (COND ((EQ (CAAR Z) ESCAPE) (GO AN1)))
57500 (SETQ ZP (CNVT2 (CAR Z)))
57600 AP1 (SETQ Z (CDR Z))
57700 (COND ((NULL Z) (GO AN2)) ((EQ (CAAR Z) ESCAPE) (GO AN1)))
57800 (SETQ ZP (LIST (QUOTE OR) (CNVT2 (CAR Z)) ZP))
57900 (GO AP1)
58000 AN1 (SETQ ZN (CNVT2 (CDAR Z)))
58100 AN1B (SETQ Z (CDR Z))
58200 AN1A (COND ((NULL Z) (GO AN2)))
58300 (SETQ ZN (LIST (QUOTE AND) (CNVT2 (CDAR Z)) ZN))
58400 (GO AN1B)
58500 AN2 (COND ((NULL ZP) (RETURN (LIST (QUOTE NOT) ZN)))
58600 ((NULL ZN) (RETURN ZP))
58700 (T (RETURN (LIST (QUOTE IMP) ZN ZP))))))
58800 EXPR)
58900
59000 (DEFPROP CNVT2
59100 (LAMBDA(X)
59200 (COND ((ATOM X) X)
59300 ((VAR (CAR X)) (CONS (CNVT3 (CAR X)) (CNVT2 (CDR X))))
59400 ((CONST (CAR X)) (CONS (CAR X) (CNVT2 (CDR X))))
59500 (T (CONS (CNVT2 (CAR X)) (CNVT2 (CDR X))))))
59600 EXPR)
59700
59800 (DEFPROP CNVT3
59900 (LAMBDA(X)
60000 (PROG (Z)
60100 (SETQ Z (ASSOC X VARL))
60200 (COND (Z (RETURN (CDR Z))))
60300 (SETQ VARL (CONS (CONS X (SETQ VARNO (ADD1 VARNO))) VARL))
60400 (RETURN VARNO)))
60500 EXPR)
60600
60700 (DEFPROP COPY
60800 (LAMBDA (X) (COND ((ATOM X) X) (T (CONS (COPY (CAR X)) (COPY (CDR X))))))
60900 EXPR)
61000
61100 (DEFPROP COPYDELETED
61200 (LAMBDA (X) (LIST (CONS (CONS NIL (CDAR X)) (CDR X))))
61300 EXPR)
61400
61500 (DEFPROP *CL
61600 (LAMBDA (C) (UPGETL1 C XYZ1 (CONS (CONS (QUOTE CLAUSES) XYZ1) NEWNAME)))
61700 EXPR)
61800
61900 (DEFPROP DEMOD
62000 (LAMBDA(X L)
62100 (PROG (S1 S2)
62200 B (SETQ S1 (CDAR X))
62300 A (COND ((NEG (CAR S1)) (DEM (TCOPY (CDR (SETQ S2 (CDAR S1)))) 1 DDEPTH L))
62400 (T (DEM (TCOPY (CDR (SETQ S2 (CAR S1)))) 1 DDEPTH L)))
62500 (COND ((EQ (CAR S2) EQUAL) (ORDEREQUAL (CDR S2))))
62600 (SETQ S1 (CDR S1))
62700 (COND (S1 (GO A)))
62800 (RETURN X)))
62900 EXPR)
63000
63100 (DEFPROP DEM
63200 (LAMBDA (T1 M N L) (COND ((OR (NULL T1) (EQ N M)) NIL) (T (PROG2 (DEM (PTRS T1) (ADD1 M) N L) (SUB* T1 L)))))
63300 EXPR)
63400
63500 (DEFPROP DEPTH
63600 (LAMBDA(Z)
63700 (PROG (Z1 Z2)
63800 (SETQ Z1 0)
63900 D1 (COND ((NEG (CAR Z)) (SETQ Z2 (CDDAR Z))) (T (SETQ Z2 (CDAR Z))))
64000 (SETQ Z1 (MAX Z1 (DEPTH1 Z2)))
64100 (SETQ Z (CDR Z))
64200 (COND (Z (GO D1)))
64300 (RETURN Z1)))
64400 EXPR)
64500
64600 (DEFPROP DEPTH
64700 (NIL . 10)
64800 VALUE)
64900
65000 (DEFPROP DEPTH1
65100 (LAMBDA(Z)
65200 (PROG (Z1)
65300 (SETQ Z1 0)
65400 D1 (COND ((OR (VAR (CAR Z)) (CONST (CAR Z))) (GO D2)))
65500 (SETQ Z1 (MAX Z1 (ADD1 (DEPTH1 (CDAR Z)))))
65600 D2 (SETQ Z (CDR Z))
65700 (COND (Z (GO D1)))
65800 (RETURN Z1)))
65900 EXPR)
66000
66100 (DEFPROP DEL
66200 (LAMBDA (C) (RPLACA (CAR C) NIL))
66300 EXPR)
66400
66500 (DEFPROP DOML
66600 (LAMBDA NIL (TERMS1 (COND ((NEG (CAR L)) (CDDAR L)) (T (CDAR L))) 100))
66700 EXPR)
66800
66900 (DEFPROP DOMC
67000 (LAMBDA NIL (CDR C))
67100 EXPR)
67200
67300 (DEFPROP DOWN
67400 (LAMBDA(N L)
67500 (PROG NIL
67600 (COND ((NOT (AND (NUMBERP N) (GREATERP N 0))) (RETURN NIL)))
67700 D1 (SETQ N (SUB1 N))
67800 (COND ((ZEROP N) (RETURN L)))
67900 (SETQ L (CDR L))
68000 (COND (L (GO D1)))
68100 (RETURN NIL)))
68200 EXPR)
68300
68400 (DEFPROP EDIT
68500 (LAMBDA(U Z)
68600 (PROG (RES1 U1 U4)
68700 ED4 (COND ((NULL Z) (RETURN RES1)))
68800 (SETQ U4 (CAR Z))
68900 (COND ((EDITSTRAT U4) (GO ED2)))
69000 (SETQ U1 SUBCLAUSES)
69100 ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
69200 ED6 (SETQ U1 (CDR U1))
69300 (COND (U1 (GO ED1)))
69400 (SETQ U1 (CDR Z))
69500 (COND ((NULL U1) (GO ED5)))
69600 ED3 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
69700 ED7 (SETQ U1 (CDR U1))
69800 (COND (U1 (GO ED3)))
69900 ED5 (SETQ RES1 (CONS U4 RES1))
70000 ED2 (SETQ Z (CDR Z))
70100 (GO ED4)))
70200 EXPR)
70300
70400 (DEFPROP ERPRINT
70500 (LAMBDA (X) (COND (DEBUG (PRINT X))))
70600 EXPR)
70700
70800 (DEFPROP ERPRIN1
70900 (LAMBDA (X) (COND (DEBUG (PRIN1 X))))
71000 EXPR)
71100
71200 (DEFPROP EXPUNGE
71300 (LAMBDA (L) (PROG NIL A (COND ((NULL L) (RETURN NIL))) (DEL (CAR L)) (SETQ L (CDR L)) (GO A)))
71400 EXPR)
71500
71600 (DEFPROP FINI
71700 (LAMBDA(U R Z1 Z2 E)
71800 (PROG (Z)
71900 (COND (UFLG (SETQ R (UNITREDUCT R UNAXP UNAXN))))
72000 (COND ((NULL R) (RETURN 0)) ((NULL (CAR R)) (PROOF Z1 Z2) (ERR (QUOTE (QED)))))
72100 (SETQ COUNT (PLUS COUNT (LENGTH R)))
72200 (SETQ R (EDIT U R))
72300 (CLAUSES2 R)
72400 (COND ((NULL R) (RETURN 0)))
72500 (BAKSUB CLAUSES R)
72600 (BOOKEEP E R (CONS Z1 Z2))
72700 (SETQ Z (UNITPN R))
72800 (SETQ UNAXP (APPEND (CAR Z) UNAXP))
72900 (SETQ UNAXN (APPEND (CDR Z) UNAXN))
73000 (RETURN (LENGTH R))))
73100 EXPR)
73200
73300 (DEFPROP FIXNEG
73400 (LAMBDA (X) (COND ((EQ (CAR X) ESCAPE) (LIST (QUOTE NOT) (COPY (CDR X)))) (T (COPY X))))
73500 EXPR)
73600
73700 (DEFPROP FIXQFF
73800 (LAMBDA(C)
73900 (PROG (Z)
74000 (SETQ Z (FIXQFF1 C NIL NIL NIL))
74100 (COND ((NULL (CAR Z)) (RETURN C)) (T (RETURN (LIST (QUOTE FA) (CAR Z) C))))))
74200 EXPR)
74300
74400 (DEFPROP FIXQFF1
74500 (LAMBDA(C NEW FA TE)
74600 (PROG (Z)
74700 (COND ((NULL C) (RETURN (CONS NEW (CONS FA TE))))
74800 ((EQ (CAR C) (QUOTE FA)) (RETURN (FIXQFF1 (CADDR C) NEW (APPEND (CADR C) FA) TE)))
74900 ((EQ (CAR C) (QUOTE TE)) (RETURN (FIXQFF1 (CADDR C) NEW FA (APPEND (CADR C) TE))))
75000 ((EQ (CAR C) (QUOTE NOT)) (RETURN (FIXQFF1 (CADR C) NEW FA TE)))
75100 ((MEMQ (CAR C) (QUOTE (AND OR IMP EQUIV))) (SETQ Z (FIXQFF1 (CADR C) NEW FA TE))
75200 (RETURN
75300 (FIXQFF1 (CADDR C) (CAR Z) (CADR Z) (CDDR Z)))))
75400 (SETQ Z (GETVARS (COND ((NEG C) (CDDR C)) (T (CDR C)))))
75500 A (COND ((NULL Z) (RETURN (CONS NEW (CONS FA TE))))
75600 ((OR (MEMBER (CAR Z) NEW) (MEMBER (CAR Z) FA) (MEMBER (CAR Z) TE)) (GO B)))
75700 (SETQ NEW (CONS (CAR Z) NEW))
75800 B (SETQ Z (CDR Z))
75900 (GO A)))
76000 EXPR)
76100
76200 (DEFPROP GENSKOLEM
76300 (LAMBDA(VARL UNL)
76400 (PROG (Z)
76500 A (COND ((NULL VARL) (RETURN Z)))
76600 (SETQ Z (CONS (CONS (CAR VARL) (CONS (MKSYM) UNL)) Z))
76700 (SETQ VARL (CDR VARL))
76800 (GO A)))
76900 EXPR)
77000
77100 (DEFPROP GETNAME
77200 (LAMBDA(X L)
77300 (PROG (Z)
77400 (SETQ Z (ASSOC X L))
77500 (COND (Z (RETURN (CDR Z))))
77600 (PRINT X)
77700 (PRINC (QUOTE IS-AN-UNBOUND-NAME))
77800 (RETURN NIL)))
77900 EXPR)
78000
78100 (DEFPROP GETTERMS
78200 (LAMBDA NIL
78300 (PROG (Z )
78400 (SCANSET)
78500 (START)
78600 (SETQ Z (ERRSET (<TM>) T))
78700 (SCANRESET)
78800 (COND ((OR (NULL Z) (NULL (CAR Z))) (RETURN NIL)))
78900 (SETQ XYZ (TOP))
79000 (COND ((NOT (EQ (READ) (QUOTE FOR))) (RETURN NIL)))
79100 (SCANSET)
79200 (START)
79300 (SETQ Z (ERRSET (<TM>) T))
79400 (SCANRESET)
79500 (COND ((OR (NULL Z) (NULL (CAR Z))) (RETURN NIL)))
79600 (SETQ XYZ1 (TOP))
79700 (COND ((NOT (EQ (READ) (QUOTE IN))) (RETURN NIL)))
79800 (RETURN (UPGETL E NAMELIST))))
79900 EXPR)
80000
80100 (DEFPROP GETVARS
80200 (LAMBDA(C)
80300 (PROG (Z)
80400 A (COND ((VAR (CAR C)) (SETQ Z (CONS (CAR C) Z)))
80500 ((CONST (CAR C)) NIL)
80600 (T (SETQ Z (APPEND (GETVARS (CDAR C)) Z))))
80700 (SETQ C (CDR C))
80800 (COND (C (GO A)))
80900 (RETURN Z)))
81000 EXPR)
81100
81200 (DEFPROP GOLIST
81300 (NIL (EO . UEO1)
81400 (DS . UDS1)
81500 (CH . UCH1)
81600 (SY . USY1)
81700 (CU . UCU1)
81800 (FL . UFL1)
81900 (DI . UDI1)
82000 (ST . UST1)
82100 (HA . UST1)
82200 (DE . UDE1)
82300 (IN . UIN1)
82400 (EV . UEV1)
82500 (QU . UQU1)
82600 (TR . UTR1)
82700 (UP . UUP1)
82800 (ME . UME1)
82900 (SI . USI1)
83000 (SE . USE1)
83100 (DO . UDO1)
83200 (CL . UCL1)
83300 (SU . USU1)
83400 (AN . UAN1)
83500 (TE . UTE1)
83600 (RE . URE1)
83700 (SA . USA1)
83800 (PA . UPA1)
83900 (AS . UAS1)
84000 (ED . UED1)
84100 (US . UUS1)
84200 (PR . UPR1)
84300 (FU . UFL2)
84400 (FD . UFL3)
84500 (GO . UGO1)
84600 (EX . UEX1)
84700 (AB . UAB1)
84800 (HE . UHE1))
84900 VALUE)
85000
85100 (DEFPROP INCLAUSES
85200 (LAMBDA NIL
85300 (PROG (Z Z1 AXNO)
85400 (SETQ AXNO (QUOTE AXIOM))
85500 A (SCANSET)
85600 (START)
85700 (SETQ ZIN (ERRSET (<INPUT>) T))
85800 (SCANRESET)
85900 (COND ((OR (NULL ZIN) (NULL (CAR ZIN))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
86000 (SETQ ZIN (TOP))
86100 (COND ((EQ ZIN (QUOTE EMPTY)) (RETURN Z))
86200 ((ATOM ZIN) (PRIN1 ZIN) (SETQ AXNO (SETQ FNNAM ZIN)) (GO A))
86300 ((MEMQ (CAR ZIN) DECOP) (GO B)))
86400 (OUT >S< ZIN)
86500 (SETQ Z
86600 (APPEND Z
86700 (SETUP
86800 (CNF
86900 (COND ((EQ AXNO (QUOTE THEOREM)) (LIST (QUOTE NOT) (FIXQFF ZIN))) (T (FIXQFF ZIN)))))))
87000 (GO A)
87100 B (SETQ Z1 (CDR (ASSOC (CAR ZIN) DECTBL)))
87200 (COND ((EQ Z1 (QUOTE IVAR)) (MAKOVAR (SETQ IVAR (APPEND IVAR (CDR ZIN)))))
87300 ((EQ Z1 (QUOTE EQUAL)) (SETQ EQUAL (CADR ZIN)))
87400 (T (SET Z1 (APPEND (CDR ZIN) (EVAL Z1)))))
87500 (OUT >INPUT< ZIN)
87600 (GO A)))
87700 EXPR)
87800
87900 (DEFPROP INITIAL
88000 (LAMBDA(L)
88100 (PROG (ST Z Z1 Z2)
88200 A (SETQ Z (CDR (ANCESTOR (CAR L))))
88300 (COND ((NOT (ATOM Z)) (PRINT (QUOTE LOSE-IN-INITIAL)) (ERR NIL))
88400 ((SETQ Z1 (ASSOC Z ST)) (RPLACD (LAST Z1) (LIST (CAR L))))
88500 (T (SETQ ST (CONS (CONS Z (LIST (CAR L))) ST))))
88600 (SETQ Z2 (CONS (CAR L) Z2))
88700 (SETQ L (CDR L))
88800 (COND (L (GO A)))
88900 (RETURN (REVERSE (CONS (CONS NIL NIL) (CONS (CONS (QUOTE %INITIAL) (REVERSE Z2)) ST))))))
89000 EXPR)
89100
89200 (DEFPROP INITIALAX
89300 (LAMBDA(L)
89400 (PROG (Z Z1 Z2 Z3 AXNO)
89500 (SETQ AXNO (CAR L))
89600 (SETQ L (CDR L))
89700 A (SETQ Z (CAR (SETUP (LIST (COPY (CDAR L))))))
89800 (SETQ Z1 (ANCESTOR (CAR L)))
89900 (COND ((ATOM (CAR Z1)) (SETQ Z1 (CDR Z1))))
90000 (SETQ Z2 (ANCESTOR Z))
90100 (RPLACA Z2 Z1)
90200 (RPLACD Z2 AXNO)
90300 (SETQ Z3 (CONS Z Z3))
90400 B (SETQ L (CDR L))
90500 (COND ((NULL L) (RETURN (REVERSE Z3))) ((ATOM (CAR L)) (SETQ AXNO (CAR L)) (GO B)))
90600 (GO A)))
90700 EXPR)
90800
90900 (DEFPROP INITIALAX1
91000 (LAMBDA(L1)
91100 (PROG (Z L2 L)
91200 (SETQ L L1)
91300 B1 (SETQ L2 L)
91400 A1 (COND ((EQ (CAR L) (CADR L2)) (RPLACD L2 (CDDR L2)) (GO A1)))
91500 (SETQ L2 (CDR L2))
91600 (COND (L2 (GO A1)))
91700 (SETQ L (CDR L))
91800 (COND (L (GO B1)))
91900 (SETQ L L1)
92000 B (SETQ Z (CDDAAR L))
92100 (COND ((NULL (CAAAR L)) (RPLACA (CAAR L) (LENGTH (CDAR L))))
92200 ((NUMBERP (CAAAR L)) NIL)
92300 (T (RPLACA (CAAR L) (CAAAAR L))))
92400 (COND ((ATOM (CDDR Z)) (GO A)))
92500 (RPLACD Z (CONS (CDR Z) (QUOTE DEDUCT)))
92600 A (SETQ L (CDR L))
92700 (COND (L (GO B)))
92800 (RETURN L1)))
92900 EXPR)
93000
93100 (DEFPROP MAKVAR
93200 (LAMBDA(X)
93300 (PROG (Z)
93400 (SETQ Z (ASSOC X VARTBL))
93500 (COND (Z (RETURN (CDR Z))))
93600 (SETQ VARTBL (CONS (CONS X (SETQ VARNO (ADD1 VARNO))) VARTBL))
93700 (RETURN VARNO)))
93800 EXPR)
93900
94000 (DEFPROP MAKOVAR
94100 (LAMBDA(X)
94200 (PROG (X1 *NOPOINT Z N M)
94300 (SETQ *NOPOINT T)
94400 (SETQ OUTVAR NIL)
94500 (SETQ N 1)
94600 (SETQ X1 X)
94700 D (SETQ OUTVAR (CONS (CONS N (CAR X1)) OUTVAR))
94800 (SETQ X1 (CDR X1))
94900 (SETQ N (ADD1 N))
95000 (COND (X1 (GO D)))
95100 B (SETQ Z (EXPLODE (CAR X)))
95200 (COND ((NUMBERP (CAR (LAST Z))) (GO A)))
95300 (SETQ M 1)
95400 C (SETQ OUTVAR (CONS (CONS N (READLIST (APPEND Z (LIST M)))) OUTVAR))
95500 (COND ((LESSP M 11) (SETQ N (ADD1 N)) (SETQ M (ADD1 M)) (GO C)))
95600 A (SETQ X (CDR X))
95700 (COND (X (SETQ N (ADD1 N)) (GO B)))
95800 (SETQ OUTVAR (REVERSE OUTVAR))
95900 (RETURN OUTVAR)))
96000 EXPR)
96100
96200 (DEFPROP MAPIT
96300 (LAMBDA(X XYZ N)
96400 (PROG (Z Z1 Z2)
96500 (SETQ Z (GETNAME X N))
96600 (COND ((NULL Z) (RETURN NIL)))
96700 A (SETQ ZIN (CAR Z))
96800 (SETQ Z2 (ERRSET (XYZ ZIN) T))
96900 (COND ((NULL Z2) (PRINT (QUOTE SCREWED-FIND)) (RETURN NIL))
97000 ((NULL (CAR Z2)) NIL)
97100 (T (SETQ Z1 (CONS (CAR Z) Z1))))
97200 (SETQ Z (CDR Z))
97300 (COND (Z (GO A)))
97400 (RETURN (REVERSE Z1))))
97500 EXPR)
97600
97700 (DEFPROP MATCHER
97800 (LAMBDA(L)
97900 (PROG (FLG Z Z1)
98000 (SETQ Z (EVAL (CADR L)))
98100 (SETQ Z1 (CAR L))
98200 (COND ((ATOM (CADR L))
98300 (COND ((MEMQ (CADR L) (QUOTE (T1 T2 T3 T4))) (SETQ FLG 4))
98400 ((MEMQ (CADR L) (QUOTE (L1 L2 L3 L4))) (SETQ FLG 3))
98500 ((MEMQ (CADR L) (QUOTE (C))) (SETQ FLG 2) (SETQ Z (CDR Z)))
98600 (T (ERR NIL))))
98700 ((EQ (CAADR L) (QUOTE TREE)) (SETQ FLG 1))
98800 (T (ERR NIL)))
98900 (COND ((ATOM Z1) (RETURN (MATCH1 Z1 Z FLG)))
99000 ((EQ (CAR Z1) (QUOTE AND)) (GO MAA1))
99100 ((EQ (CAR Z1) (QUOTE OR)) (GO MAO1))
99200 (T (RETURN (MATCH1 Z1 Z FLG))))
99300 MAA1 (SETQ Z1 (CDR Z1))
99400 MAAND
99500 (COND ((NULL Z1) (RETURN T)) ((MATCH1 (CAR Z1) Z FLG) (GO MAA1)) (T (RETURN NIL)))
99600 MAO1 (SETQ Z1 (CDR Z1))
99700 MAOR (COND ((NULL Z1) (RETURN NIL)) ((MATCH1 (CAR Z1) Z FLG) (RETURN T)))
99800 (GO MAO1)))
99900 FEXPR)
00100
00200 (DEFPROP MATCH1
00300 (LAMBDA(X Y FL)
00400 (COND ((ATOM X)
00500 (COND ((EQ X (QUOTE %NG)) (COND ((ISLIT FL) (NEG Y)) ((ISCL FL) (MATCHPN Y T)) (T (ERR NIL))))
00600 ((EQ X (QUOTE %PL)) (COND ((ISLIT FL) (NOT (NEG Y))) ((ISCL FL) (MATCHPN Y NIL)) (T (ERR NIL))))
00700 ((NUMBERP X) (COND ((ISCLS FL) (MATCHTR X Y)) (T (MATMLT X Y FL))))
00800 ((AND (MEMQ X (QUOTE (C1 C2))) (ISCLS FL)) (MEMQ (EVAL X) Y))
00900 (T (ERR NIL))))
01000 ((NUMBERP (CAR X)) (COND ((ISCLS FL) (MATCHTR (CAR X) Y)) (T (MATMLT (CAR X) Y FL))))
01100 ((EQ (LENGTH X) 1) (MATMLT (CAR X) Y FL))
01200 ((ISCLS FL) NIL)
01300 (T (MATMLT* X Y FL))))
01400 EXPR)
01500
01600 (DEFPROP MATCHTR
01700 (LAMBDA (N TR) (MEMQ (CAR (DOWN N CLAUSES)) TR))
01800 EXPR)
01900
02000 (DEFPROP MATCHPN
02100 (LAMBDA(X FL)
02200 (PROG (Z)
02300 A (SETQ Z (NEG (CAR X)))
02400 (COND ((AND Z FL) (RETURN T)) ((AND (NOT Z) (NOT FL)) (RETURN T)))
02500 (SETQ X (CDR X))
02600 (COND (X (GO A)))
02700 (RETURN NIL)))
02800 EXPR)
02900
03000 (DEFPROP MATMLT
03100 (LAMBDA(X Y FL)
03200 (PROG NIL
03300 (COND ((AND (ISTRM FL) (NOT (ASSOC X TBL))) (ERR NIL))
03400 ((ISTRM FL) (RETURN (OCR X Y)))
03500 ((ISLIT FL) (RETURN (COND ((NEG Y) (OCR X (CDR Y))) (T (OCR X Y))))))
03600 A (COND ((COND ((NEG (CAR Y)) (OCR X (CDAR Y))) (T (OCR X (CAR Y)))) (RETURN T)))
03700 (SETQ Y (CDR Y))
03800 (COND (Y (GO A)))
03900 (RETURN NIL)))
04000 EXPR)
04100
04200 (DEFPROP MATMLT*
04300 (LAMBDA(X Y FL)
04400 (PROG (Z)
04500 (COND ((AND (ISTRM FL) (NOT (ASSOC (CAR X) TBL))) (ERR NIL))
04600 ((EQ (CAR X) (QUOTE %NG)) (SETQ X (CDR X)) (GO M1))
04700 ((NOT (ISCL FL)) (SETQ Y (LIST Y))))
04800 D (SETQ X (VARIT (LIST X)))
04900 B (SETQ Z (TERMS1 (LIST (COND ((NEG (CAR Y)) (CDAR Y)) (T (CAR Y)))) 64))
05000 A (COND ((UNI X (CAR Z) NIL) (RETURN T)))
05100 (SETQ Z (CDR Z))
05200 (COND (Z (GO A)))
05300 (SETQ Y (CDR Y))
05400 (COND (Y (GO B)))
05500 (RETURN NIL)
05600 M1 (COND ((NEG (CAR Y)) (GO M2)))
05700 M3 (SETQ Y (CDR Y))
05800 (COND (Y (GO M1)))
05900 (RETURN NIL)
06000 M2 (COND ((EQ (LENGTH X) 1) (COND ((EQ (CADAR Y) (CAR X)) (RETURN T)) (T (GO M3)))) (T (GO D)))))
06100 EXPR)
06200
06300 (DEFPROP MAX
06400 (LAMBDA (X Y) (COND ((GREATERP X Y) X) (T Y)))
06500 EXPR)
06600
06700 (DEFPROP MEMC
06800 (LAMBDA(C L)
06900 (PROG NIL
07000 (COND ((NULL L) (RETURN NIL)) ((POS C) (GO A)))
07100 B (COND ((POS (CAR L)) (RETURN NIL)) ((EQUAL C (CAR L)) (RETURN T)))
07200 (SETQ L (CDR L))
07300 (COND (L (GO B)))
07400 (RETURN NIL)
07500 A (COND ((POS (CAR L)) (RETURN (MEMBER C L))))
07600 (SETQ L (CDR L))
07700 (COND (L (GO A)))
07800 (RETURN NIL)))
07900 EXPR)
08000
08100 (DEFPROP MIN1
08200 (LAMBDA(L)
08300 (PROG (Z Z1)
08400 (SETQ Z (CAR L))
08500 M1 (SETQ Z1 (CDR L))
08600 (COND ((NULL Z1)
08700 (COND ((NUMBERP (CAR Z)) (RETURN NIL)) (T (SETQ Z1 (COPY Z)) (RPLACA Z 0) (RETURN Z1))))
08800 ((NUMBERP (CAAR Z1)) (GO M2))
08900 ((OR (NUMBERP (CAR Z)) (ORDER Z (CAR Z1))) (SETQ Z (CAR Z1))))
09000 M2 (SETQ L (CDR L))
09100 (GO M1)))
09200 EXPR)
09300
09400 (DEFPROP MINIMIZE
09500 (LAMBDA(Z3)
09600 (PROG (Z1 Z2 Z4)
09700 (SETQ Z2 (LIST (CAR Z3)))
09800 ED2 (SETQ Z3 (CDR Z3))
09900 (COND ((NULL Z3) (RETURN (REVERSE Z2))))
10000 (SETQ Z4 (CAR Z3))
10100 (SETQ Z1 Z2)
10200 ED1 (COND ((SUBSUME (CAR Z1) Z4) (GO ED2)))
10300 (SETQ Z1 (CDR Z1))
10400 (COND (Z1 (GO ED1)))
10500 (SETQ Z1 (CDR Z3))
10600 ED4 (COND ((NULL Z1) (GO ED5)) ((SUBSUME (CAR Z1) Z4) (GO ED2)))
10700 (SETQ Z1 (CDR Z1))
10800 (GO ED4)
10900 ED5 (SETQ Z2 (CONS Z4 Z2))
11000 (GO ED2)))
11100 EXPR)
11200
11300 (DEFPROP MIN
11400 (LAMBDA (X Y) (COND ((LESSP X Y) X) (T Y)))
11500 EXPR)
11600
11700 (DEFPROP MKSYM
11800 (LAMBDA NIL
11900 (PROG NIL
12000 (SETQ FNLIST (CONS (READLIST (APPEND (EXPLODE FNNAM) (EXPLODE (SETQ FNNO (ADD1 FNNO))))) FNLIST))
12100 (SETQ PREFN (CONS (CAR FNLIST) PREFN))
12200 (RETURN (CAR FNLIST))))
12300 EXPR)
12400
12500 (DEFPROP MODEL
12600 (LAMBDA(C)
12700 (PROG (Z)
12800 (SETQ Z (CDR C))
12900 M1 (COND ((NEG (CAR Z)) (GO M3)) ((MEMBER (CAAR Z) PMODEL) (SETQ SAT C) (RETURN T)))
13000 M2 (SETQ Z (CDR Z))
13100 (COND (Z (GO M1)))
13200 (RETURN NIL)
13300 M3 (COND ((MEMBER (CADAR Z) NMODEL) (SETQ SAT C) (RETURN T)))
13400 (GO M2)))
13500 EXPR)
13600
13700 (DEFPROP NCONC1
13800 (LAMBDA (A B) (COND ((NULL A) B) ((NULL B) A) (T (RPLACD A B))))
13900 EXPR)
14000
14100 (DEFPROP NEGATE
14200 (LAMBDA(Z)
14300 (PROG (BDY)
14400 A (SETQ Z (CDR Z))
14500 (COND ((EQ (LENGTH Z) 1) (SETQ BDY (FIXNEG (CAR Z))) (GO D)))
14600 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CADR Z)) (FIXNEG (CAR Z))))
14700 (SETQ Z (CDDR Z))
14800 C (COND ((NULL Z) (GO D)))
14900 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CAR Z)) BDY))
15000 (SETQ Z (CDR Z))
15100 (GO C)
15200 D (RETURN (SET3 (SETUP (CNF (LIST (QUOTE NOT) (FIXQFF BDY))))))))
15300 EXPR)
15400
15500 (DEFPROP NEGSGN
15600 (NIL . ¬)
15700 VALUE)
15800
15900 (DEFPROP NOSYM
16000 (LAMBDA (L) (COND ((NULL L) 0) ((ATOM L) 1) (T (MAX (ADD1 (NOSYM (CAR L))) (NOSYM (CDR L))))))
16100 EXPR)
16200
16300 (DEFPROP OCR
16400 (LAMBDA (X Y) (OCR1 X (LIST Y)))
16500 EXPR)
16600
16700 (DEFPROP OCR1
16800 (LAMBDA(X Y)
16900 (COND ((NULL Y) NIL)
17000 ((VAR (CAR Y)) (OCR1 X (CDR Y)))
17100 ((CONST (CAR Y)) (COND ((EQ (CAAR Y) X) T) (T (OCR1 X (CDR Y)))))
17200 ((EQ X (CAAR Y)) T)
17300 ((OCR1 X (CDAR Y)) T)
17400 (T (OCR1 X (CDR Y)))))
17500 EXPR)
17600
17700 (DEFPROP ONEGSGN
17800 (NIL . ¬)
17900 VALUE)
18000
18100 (DEFPROP *NOPOINT
18200 (NIL . T)
18300 VALUE)
18400
18500 (DEFPROP OCCUR
18600 (LAMBDA(X Z)
18700 (PROG (Z1)
18800 OC1 (SETQ Z1 (CAR Z))
18900 (COND ((VAR Z1) (COND ((EQ X Z1) (RETURN T)) (T (GO OC2))))
19000 ((CONST Z1) (GO OC2))
19100 ((OCCUR X (CDR Z1)) (RETURN T)))
19200 OC2 (SETQ Z (CDR Z))
19300 (COND (Z (GO OC1)))
19400 (RETURN NIL)))
19500 EXPR)
19600
19700 (DEFPROP ORDER
19800 (LAMBDA(X Y)
19900 (COND ((POS X) (COND ((POS Y) (ORDERP (CAR X) (CAR Y))) (T T)))
20000 ((NEG X) (COND ((NEG Y) (ORDERP (CADR X) (CADR Y))) (T NIL)))))
20100 EXPR)
20200
20300 (DEFPROP ORDEREQUAL
20400 (LAMBDA(S)
20500 (PROG NIL
20600 (COND ((VAR (CAR S))
20700 (COND ((VAR (CADR S)) (COND ((GREATERP (CADR S) (CAR S)) (GO A)) (T (RETURN NIL)))) (T (GO A))))
20800 ((CONST (CAR S))
20900 (COND ((VAR (CADR S)) (RETURN NIL))
21000 ((CONST (CADR S)) (COND ((ORDERP (CAAR S) (CAADR S)) (GO A)) (T (RETURN NIL))))
21100 (T (GO A))))
21200 ((OR (VAR (CADR S)) (CONST (CADR S))) (RETURN NIL))
21300 ((GREATERP (DEPTH1 (CDAR S)) (DEPTH1 (CDADR S))) (RETURN NIL)))
21400 A (PROG (S1) (SETQ S1 (CADR S)) (RPLACA (CDR S) (CAR S)) (RPLACA S S1))))
21500 EXPR)
21600
21700 (DEFPROP PARMOD
21800 (LAMBDA(C D)
21900 (COND ((ALLNEG C) (PARMOD1 D C)) ((ALLNEG D) (PARMOD1 C D)) (T (NCONC (PARMOD1 C D) (PARMOD1 D C)))))
22000 EXPR)
22100
22200 (DEFPROP PARMOD1
22300 (LAMBDA(C D)
22400 (PROG (YC YD Z Z1 Z2 X Y Y1 Y2 PAR TS)
22500 (SETQ YC (CDR C))
22600 PAR1 (SETQ YD (CDR D))
22700 (SETQ X (CAR YC))
22800 (COND ((NEG X) (RETURN PAR))
22900 ((ORDERP (CAR X) EQUAL) (GO PAR2))
23000 ((NOT (EQ (CAR X) EQUAL)) (RETURN PAR)))
23100 PAR3 PAR3A
23200 (COND ((NEG (CAR YD)) (SETQ Z2 (CDAR YD))) (T (SETQ Z2 (CAR YD))))
23300 (SETQ Y1 (CDDR X))
23400 (SETQ Y2 (CADR X))
23500 PAR3B
23600 (COND ((VAR (CAR Y1)) (GO PAR7A)))
23700 (SETQ Z (TERMS (CAAR Y1) (CDR Z2) PDEPTH))
23800 (COND ((NULL Z) (GO PAR7A)))
23900 PAR5 (SETQ Z1 Z)
24000 PAR4 (COND
24100 ((CONST (CAR Y1))
24200 (COND ((OR (VAR (CAAR Z1)) (NOT (EQ (CAAR Y1) (CAAAR Z1)))) (GO PAR7))
24300 (T (SETQ TS (COPY Y2)) (GO PAR9))))
24400 ((OR (VAR (CAAR Z1)) (NOT (EQ (CAAR Y1) (CAAAR Z1)))) (GO PAR7)))
24500 (SETQ Y (UNIFY (CDAR Y1) (CDAAR Z1)))
24600 (COND (Y (SETQ Y (CDR Y)) (GO PAR6)))
24700 PAR7 (SETQ Z1 (CDR Z1))
24800 (COND (Z1 (GO PAR4)))
24900 PAR7A
25000 PAR7B
25100 (SETQ YD (CDR YD))
25200 (COND (YD (GO PAR3A)))
25300 PAR2 (SETQ YC (CDR YC))
25400 (COND (YC (GO PAR1)))
25500 (RETURN PAR)
25600 PAR6 (SETQ TS (CADR (SUBS3T* Y (LIST NIL Y2))))
25700 PAR9 (SETQ PARRES (SUBS3TA Y Z2 (CAR Z1) TS))
25800 (COND ((NEG (CAR YD)) (SETQ PARRES (CONS ESCAPE PARRES))))
25900 (SETQ Y (UNION Y C D X (CAR YD)))
26000 (COND ((NULL Y) (GO PAR7)))
26100 (SETQ PAR (CONS (SET2 (CAR Y) TBL) PAR))
26200 (GO PAR7)))
26300 EXPR)
26400
26500 (DEFPROP POTZ
26600 (LAMBDA(X)
26700 (PROG (Z Z1)
26800 (SETQ Z (POTZ1 X))
26900 (COND ((SETQ Z1 (PMEMQ Z POTZTBL)) (RETURN Z1)))
27000 (SETQ POTZTBL (CONS Z POTZTBL))
27100 (RETURN Z)))
27200 EXPR)
27300
27400 (DEFPROP PRECNF
27500 (LAMBDA(X)
27600 (COND ((EQ (CAR X) (QUOTE NOT)) (LIST (QUOTE NOT) (PRECNF (CADR X))))
27700 ((MEMQ (CAR X) (QUOTE (AND OR))) (LIST (CAR X) (PRECNF (CADR X)) (PRECNF (CADDR X))))
27800 ((MEMQ (CAR X) (QUOTE (FA TE))) (LIST (CAR X) (CADR X) (PRECNF (CADDR X))))
27900 ((EQ (CAR X) (QUOTE IMP)) (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X))))
28000 ((EQ (CAR X) (QUOTE EQUIV))
28100 (LIST (QUOTE AND)
28200 (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X)))
28300 (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (COPY (CADDR X)))) (PRECNF (COPY (CADR X))))))
28400 (T X)))
28500 EXPR)
28600
28700 (DEFPROP PROOF1
28800 (LAMBDA(L)
28900 (PROG (Q X Y Z P P1)
29000 (PRINC (QUOTE / ))
29100 (PRINC (QUOTE / ))
29200 (PRFPRINT (CDR L))
29300 (SETQ P (ANCESTOR L))
29400 (COND ((ATOM (CDR P)) (GO P3)))
29500 (SETQ P1 (CDR P))
29600 (SETQ P (CAR P))
29700 (PRINC (QUOTE / ))
29800 (PRINC 1)
29900 (PRINC (QUOTE / ))
30000 (PRINC 2)
30100 (SETQ X 1)
30200 (SETQ Y 2)
30300 (SETQ Q (LIST (CONS X P) (CONS Y P1)))
30400 P1 (SETQ Z (ANCESTOR (CDAR Q)))
30500 (COND ((ATOM (CDR Z)) (PRINT (CAAR Q)) (PRFPRINT (CDDAR Q)) (PRIN1 (CDR Z)) (GO P2)))
30600 (SETQ X (ADD1 Y))
30700 (SETQ Y (ADD1 X))
30800 (PRINT (CAAR Q))
30900 (PRFPRINT (CDDAR Q))
31000 (PRINC X)
31100 (PRINC (QUOTE / ))
31200 (PRINC Y)
31300 (SETQ Q (NCONC Q (LIST (CONS X (CAR Z)) (CONS Y (CDR Z)))))
31400 P2 (SETQ Q (CDR Q))
31500 (COND ((NULL Q) (RETURN NIL)))
31600 (GO P1)
31700 P3 (PRIN1 (CDR P))
31800 (RETURN (TERPRI))))
31900 EXPR)
32000
32100 (DEFPROP PROVE
32200 (LAMBDA (L) (PROG (AUTO) (SETQ AUTO T) (EVAL (CONS (QUOTE TRY1) L))))
32300 FEXPR)
32400
32500 (DEFPROP PRPAR
32600 (LAMBDA(L)
32700 (PROG NIL
32800 (CLAUSES CLAUSES)
32900 (TERPRI)
33000 P1 (PROOF1 (CAR L))
33100 (TERPRI)
33200 (TERPRI)
33300 (SETQ L (CDR L))
33400 (COND (L (GO P1)))
33500 (RETURN NIL)))
33600 EXPR)
33700
33800 (DEFPROP PRFPRINT
33900 (LAMBDA(X)
34000 (PROG NIL
34100 (SETQ &&Z (FUNFLAT (LIST (LIST (OUTTST (CNVT X) (FUNCTION >S<))))))
34200 (SETQ LAST NIL)
34300 (FPRINT &&Z 0)))
34400 EXPR)
34500
34600 (DEFPROP PRFPR1
34700 (LAMBDA(L)
34800 (PROG (Z)
34900 (COND ((NEG L) (PRINC ONEGSGN) (SETQ L (CDR L))))
35000 (PRINC (CAR L))
35100 (SETQ L (CDR L))
35200 (PRINC (QUOTE /())
35300 P1 (COND ((VAR (CAR L))
35400 (COND ((MINUSP (CAR L)) (PRINC (QUOTE Z)) (PRINC (MINUS (CAR L))))
35500 (T (PRINC (QUOTE X))
35600 (COND ((SETQ Z (ASSOC (CAR L) VARL)) (PRINC (CDR Z)))
35700 (T (SETQ VARL (CONS (CONS (CAR L) (SETQ ONO (ADD1 ONO))) VARL)) (PRINC ONO))))))
35800 ((CONST (CAR L)) (PRINC (CAAR L)))
35900 (T (PRFPR1 (CAR L))))
36000 P2 (SETQ L (CDR L))
36100 (COND ((NULL L) (PRINC (QUOTE /))) (RETURN NIL)))
36200 (PRINC (QUOTE /,))
36300 (GO P1)))
36400 EXPR)
36500
36600 (DEFPROP PROOF
36700 (LAMBDA(L R)
36800 (PROG (Q Q1 X Z)
36900 (SETQ LHP L)
37000 (SETQ RHP R)
37100 (RPLACA (MKWRD L) 1)
37200 (RPLACA (MKWRD R) 2)
37300 (SETQ X 2)
37400 (SETQ Q (LIST L R))
37500 (SETQ Q1 Q)
37600 P1 (SETQ Z (ANCESTOR (CAR Q)))
37700 (COND ((ATOM (CDR Z)) (COND ((NOT (ATOM (CAR Z))) (SETQ Z (CAR Z))) (T (GO P2)))))
37800 (RPLACA (MKWRD (CAR Z)) (SETQ X (ADD1 X)))
37900 (RPLACA (MKWRD (CDR Z)) (SETQ X (ADD1 X)))
38000 (NCONC Q (LIST (CAR Z) (CDR Z)))
38100 P2 (SETQ Q (CDR Q))
38200 (COND (Q (GO P1)))
38300 (PRINT (QUOTE NIL))
38400 (PRINC (CAR (MKWRD (CAR Q1))))
38500 (PRINC (QUOTE / ))
38600 (PRINC (CAR (MKWRD (CADR Q1))))
38700 (SETQ X 1)
38800 A (COND
38900 ((EQ (CAR (MKWRD (CAR Q1))) X) (PRINT X)
39000 (PRFPRINT (CDAR Q1))
39100 (COND
39200 ((ATOM (CAR (ANCESTOR (CAR Q1)))) (PRIN1 (CAR (ANCESTOR (CAR Q1)))))
39300 ((ATOM (CDR (ANCESTOR (CAR Q1))))
39400 (PRINC (CAR (MKWRD (CAAR (ANCESTOR (CAR Q1))))))
39500 (PRINC (QUOTE / ))
39600 (PRINC (CAR (MKWRD (CDAR (ANCESTOR (CAR Q1)))))))
39700 (T (PRINC (CAR (MKWRD (CAR (ANCESTOR (CAR Q1))))))
39800 (PRINC (QUOTE / ))
39900 (PRINC (CAR (MKWRD (CDR (ANCESTOR (CAR Q1))))))))))
40000 (SETQ Q1 (CDR Q1))
40100 (SETQ X (ADD1 X))
40200 (COND (Q1 (GO A)))))
40300 EXPR)
40400
40500 (DEFPROP PTRS
40600 (LAMBDA(X)
40700 (PROG (Z)
40800 A (COND ((VAR (CAAR X)) NIL) ((CONST (CAAR X)) NIL) (T (SETQ Z (APPEND (TCOPY (CDAAR X)) Z))))
40900 (SETQ X (CDR X))
41000 (COND (X (GO A)))
41100 (RETURN Z)))
41200 EXPR)
41300
41400 (DEFPROP PUNIFY
41500 (LAMBDA(X Y)
41600 (PROG (LC Z1 Z2 Z3 Z4 Z6 Z7)
41700 (SETQ LC (LIST NIL))
41800 U3 (SETQ Z1 (CAR X))
41900 (SETQ Z2 (CAR Y))
42000 (COND ((VAR Z1) (SETQ Z3 (SEARCH Z1 (CDR LC)))) (T (SETQ Z3 Z1)))
42100 (COND ((VAR Z2) (SETQ Z4 (SEARCH Z2 (CDR LC)))) (T (SETQ Z4 Z2)))
42200 (COND ((VAR Z3)
42300 (COND ((VAR Z4) (GO UN1))
42400 ((CONST Z4) (GO UN3))
42500 (T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z3 (COPY Z4)))) (GO UN2))
42600 ((NOT (VAR Z2)) (SETQ Z4 (SUBS3T* (CDR LC) Z4))))
42700 (COND ((OCCUR Z3 (CDR Z4)) (RETURN NIL)) (T (GO UN3))))))
42800 ((VAR Z4) (RETURN NIL))
42900 ((AND (CONST Z3) (CONST Z4)) (COND ((NOT (EQ (CAR Z3) (CAR Z4))) (RETURN NIL)) (T (GO UN2))))
43000 ((EQ (CAR Z3) (CAR Z4)) (SETQ Z6 (CDR (SUBS3T* (CDR LC) Z3)))
43100 (SETQ Z7 (CDR (SUBS3T* (CDR LC) Z4)))
43200 (SETQ X (APPEND Z6 (CDR X)))
43300 (SETQ Y (APPEND Z7 (CDR Y)))
43400 (GO U3))
43500 (T (RETURN NIL)))
43600 UN1 (SUBS2T Z3 Z4 LC)
43700 UN2 (SETQ X (CDR X))
43800 (COND (X (SETQ Y (CDR Y)) (GO U3)))
43900 (RETURN LC)
44000 UN3 (SUBS2T Z4 Z3 LC)
44100 (GO UN2)))
44200 EXPR)
44300
44400 (DEFPROP QUERY
44500 (LAMBDA NIL
44600 (PROG NIL
44700 (PRINT (QUOTE CHOICE-STRATEGY-IS:))
44800 (OUTIT SAVESTR)
44900 (PRINT (QUOTE EDIT-STRATEGY-IS:))
45000 (OUTIT (CAR (LAST EDITSTRAT)))
45100 (PRINT (QUOTE ELAPSED-TIME))
45200 (PRINC (QUOTE =))
45300 (PRINC (TIMEIT))
45400 (RETURN (TERPRI))))
45500 EXPR)
45600
45700 (DEFPROP REAL-LNGTH
45800 (LAMBDA(L)
45900 (PROG (N)
46000 (SETQ N 0)
46100 A (COND ((NULL (CDR L)) (RETURN N)) ((HERE (CAR L)) (SETQ N (ADD1 N))))
46200 (SETQ L (CDR L))
46300 (GO A)))
46400 EXPR)
46500
46600 (DEFPROP REDUCER
46700 (LAMBDA(C L)
46800 (PROG (Z Z1 Z2 Z3 C1)
46900 (SETQ Z (CDAR C))
47000 (SETQ Z2 (CDAAR C))
47100 (SETQ C1 C)
47200 (SETQ Z3 (SETQ Z1 (CONS NIL (CAR Z2))))
47300 A (COND ((EQ L (CDR C1)) (GO B)))
47400 (SETQ C1 (CDR C1))
47500 (SETQ Z1 (CDR Z1))
47600 (GO A)
47700 B (RPLACD C1 (CDDR C1))
47800 (COND ((EQ (CAR Z) L) (RPLACA Z (CDR L))))
47900 (COND ((EQ (CDR Z2) (CDR Z1)) (RPLACD Z2 (CDDR Z2))))
48000 (RPLACD Z1 (CDDR Z1))
48100 (RPLACA Z2 (CDR Z3))
48200 (RPLACA (CAAR C) (SUB1 (CAAAR C)))
48300 (RETURN C)))
48400 EXPR)
48500
52100
52200 (DEFPROP RESOLVE
52300 (LAMBDA(C D)
52400 (COND ((OR (ALLNEG D) (ALLPOS C)) (RESOLVE1 C D))
52500 ((OR (ALLPOS D) (ALLNEG C)) (RESOLVE1 D C))
52600 (T (NCONC (RESOLVE1 C D) (RESOLVE1 D C)))))
52700 EXPR)
52800
52900 (DEFPROP RESOLVE1
53000 (LAMBDA(C D)
53100 (PROG (CB DB DB1 YC YD YD1 Z X Y RES)
53200 (COND ((AND COND (EVAL COND)) (ERR (CDR LCL))))
53300 (SETQ YC (CDR C))
53400 (SETQ CB (POSBIT C))
53500 (SETQ YD1 (NEGL D))
53600 (SETQ DB1 (NEGBIT D))
53700 (SETQ DB DB1)
53800 (SETQ YD YD1)
53900 RES1 (SETQ X (CAR YC))
54000 (COND ((NEG X) (RETURN RES)))
54100 (SETQ Y (CAR YD))
54200 (COND ((ORDERP (CAR X) (CADR Y)) (GO RES3)) ((NOT (EQ (CAR X) (CADR Y))) (GO RES4)))
54300 (SETQ YD1 YD)
54400 (SETQ DB1 DB)
54500 (GO RES2A)
54600 RES2 (SETQ Y (CAR YD))
54700 (COND ((NOT (EQ (CAR X) (CADR Y))) (GO RES3A)))
54800 RES2A
54900 (COND ((NOT (UNIFAB (CAR CB) (CAR DB))) (GO RES2B)))
55000 (SETQ Z (UNIFY (CDR X) (CDDR Y)))
55100 (COND ((NULL Z) (GO RES2B)))
55200 (SETQ PARRES NIL)
55300 (SETQ Z (UNION (CDR Z) C D X Y))
55400 (COND ((NULL Z) (GO RES2B)) ((NULL (CAR Z)) (RETURN Z)))
55500 (SETQ RES (CONS (SET2 (CAR (COND (DLIST (DEMOD Z DLIST)) (T Z))) TBL) RES))
55600 RES2B
55700 (SETQ YD (CDR YD))
55800 (COND (YD (SETQ DB (CDR DB)) (GO RES2)))
55900 RES3A
56000 (SETQ DB DB1)
56100 (SETQ YD YD1)
56200 RES3 (SETQ YC (CDR YC))
56300 (COND (YC (SETQ CB (CDR CB)) (GO RES1)))
56400 (RETURN RES)
56500 RES4 (SETQ YD (CDR YD))
56600 (COND (YD (SETQ DB (CDR DB)) (GO RES1)))
56700 (GO RES3A)))
56800 EXPR)
56900
58200
58300 (DEFPROP RESET
58400 (LAMBDA(L)
58500 (PROG (Z) R1 (SETQ Z (EVAL (CONS (QUOTE RESET1) (CAR L)))) (SETQ L (CDR L)) (COND (L (GO R1))) (RETURN Z)))
58600 FEXPR)
58700
58800 (DEFPROP RESET
58900 (LAMBDA (L) (PROG2 (SYSIN TRACE) (LIST (QUOTE QUOTE) (EVAL L))))
59000 MACRO)
59100
59200 (DEFPROP RESET1
59300 (LAMBDA(L)
59400 (PROG (X Z2 Z3 ZZ XX Z Z1 F1)
59500 (SETQ Z STATEVECTOR)
59600 A (COND
59700 ((EQ (CAR L) (CAR Z)) (SETQ F1 T)
59800 (COND ((EQ (CAR L) (QUOTE STRATEGY)) (GO R1))
59900 (T (SET (CAR Z) (EVAL (CADR L)))))))
60000 R2 (SETQ Z1 (CONS (EVAL (CAR Z)) Z1))
60100 (SETQ Z (CDR Z))
60200 (COND (Z (GO A)))
60300 (COND (F1 (RETURN (REVERSE Z1))))
60400 R3 (PRINT (QUOTE UNDEFINED-ARG-FOR-RESET:))
60500 (PRINC (CAR L))
60600 (TERPRI)
60700 (ERR NIL)
60800 R1 (SETQ X (QUOTE (X)))
60900 (SETQ L (CDR L))
61000 R4 (SETQ Z2 (CAR L))
61100 (COND ((ATOM Z2) (SETQ Z3 Z2)) (T (SETQ Z3 (CAR Z2))))
61200 SPQ2 (COND ((NOT (MEMQ Z3 STRATLIST)) (GO R3))
61300 ((EQ Z3 (QUOTE SUPPORT)) (SETQ XX (EVAL (CADAR L)))
61400 (PROG (ZZ)
61500 (GO B)
61600 A (SETQ ZZ (CONS (CDAR XX) ZZ))
61700 (SETQ XX (CDR XX))
61800 B (COND (XX (GO A)))
61900 (SETQ SUPPORT ZZ))
62000 (SETQ ZZ (QUOTE (SUPPORT C2))))
62100 ((EQ Z3 (QUOTE MODEL)) (SETQ PMODEL (CADAR L))
62200 (SETQ NMODEL (CADDAR L))
62300 (SETQ ZZ (CONS (CONS Z3 X) ZZ)))
62400 ((EQ Z3 (QUOTE ANCESTRY)) (SETQ ANCESTRY T))
62500 ((EQ Z3 (QUOTE ORDER)) (SETQ ORDER T))
62600 ((EQ Z3 (QUOTE MERGE)) (SETQ MERGE T))
62700 (T (SETQ ZZ (CONS (CONS Z3 X) ZZ))))
62800 (SETQ L (CDR L))
62900 (COND (L (GO R4)))
63000 (COND (ZZ (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (SUPPORT C2))))) (T (SETQ STRATEGY NIL)))
63100 (GO R2)))
63200 FEXPR)
63300
68500
68600 (DEFPROP SET1
68700 (LAMBDA(L)
68800 (PROG (TBL N)
68900 (SETQ N 1)
69000 (SETQ ZERO (CDAR (SETU (LIST (CONS 0 0)))))
69100 A (SETQ TBL (CONS (CONS (CAR L) N) TBL))
69200 (SETQ L (CDR L))
69300 (COND (L (SETQ N (ADD1 N)) (GO A)))
69400 (RETURN (SETU TBL))))
69500 EXPR)
69600
69700 (DEFPROP SET2
69800 (LAMBDA(C L)
69900 (PROG (X Z T1 T2 T3* T2* T3 Z1)
70000 (SETQ T2 (SETQ T2* (LIST NIL)))
70100 (SETQ T3 (SETQ T3* (LIST NIL)))
70200 (SETQ X (CDR C))
70300 S1 (SETQ Z (CDAR X))
70400 (SETQ T1 NIL)
70500 (COND ((NEG (CAR X)) (GO S2)))
70600 S1A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
70700 ((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
70800 (T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
70900 (SETQ T1 (CONS (CDAR (LAST L)) T1))))
71000 (SETQ Z (CDR Z))
71100 (COND (Z (GO S1A)))
71200 (SETQ X (CDR X))
71300 (RPLACD T2* (LIST (POTZ T1)))
71400 (SETQ T2* (CDR T2*))
71500 (COND (X (GO S1)))
71600 S4 (COND ((EQ T2 T2*) (RPLACA T3 (CDR T3))) (T (RPLACA T3 (CDR T2)) (RPLACD T2* (CDR T3))))
71700 (RPLACA (CAR C) (CONS (CAAR C) T3))
71800 (RETURN C)
71900 S2 (SETQ Z (CDDAR X))
72000 (SETQ T1 NIL)
72100 S2A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
72200 ((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
72300 (T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
72400 (SETQ T1 (CONS (CDAR (LAST L)) T1))))
72500 (SETQ Z (CDR Z))
72600 (COND (Z (GO S2A)))
72700 (SETQ X (CDR X))
72800 (RPLACD T3* (LIST (POTZ T1)))
72900 (SETQ T3* (CDR T3*))
73000 (COND (X (GO S2)))
73100 (GO S4)))
73200 EXPR)
73300
73400 (DEFPROP SET3
73500 (LAMBDA(Z)
73600 (PROG (E)
73700 (COND ((OR (NULL Z) (MEMQ NIL Z)) (RETURN Z)))
73800 (SETQ E Z)
73900 S1 (COND ((HERE (CAR E)) (SET2 (CAR E) TBL)))
74000 (SETQ E (CDR E))
74100 (COND (E (GO S1)))
74200 (RETURN Z)))
74300 EXPR)
74400
74500 (DEFPROP SETUP
74600 (LAMBDA(Z)
74700 (PROG (BL Z1 Z2 Z3 Z4 Z5)
74800 SET2 (SETQ Z3 (CAR Z))
74900 (SETQ Z2 0)
75000 (SETQ BL NIL)
75100 (SETQ NO* NO)
75200 (SETQ Z5 NIL)
75300 S1 (SETQ Z4 (MIN1 Z3))
75400 (COND ((NULL Z4) (GO S3)))
75500 (UPIT Z4)
75600 (COND ((MEMBER Z4 Z5) (GO S1)) ((POS Z4) (COND ((MEMBER (CONS ESCAPE Z4) Z5) (GO S4)))))
75700 (SETQ Z2 (ADD1 Z2))
75800 (SETQ Z5 (CONS Z4 Z5))
75900 (GO S1)
76000 S3 (SETQ Z3 NIL)
76100 (SETQ Z4 Z5)
76200 S2 (COND ((NEG (CAR Z4)) (SETQ Z3 Z4) (GO SET3)))
76300 (SETQ Z4 (CDR Z4))
76400 (COND (Z4 (GO S2)))
76500 SET3 (SETQ Z5 (CONS (CONS Z2 (CONS Z3 (CONS 0 (CONS AXNO AXNO)))) Z5))
76600 SET1 (SETQ Z1 (CONS Z5 Z1))
76700 S4 (SETQ Z (CDR Z))
76800 (COND (Z (GO SET2)))
76900 (RETURN Z1)))
77000 EXPR)
77100
77200 (DEFPROP SEARCH2
77300 (LAMBDA (X L L1) (PROG NIL (SETQ KR1 (ASSOC X L)) (COND (KR1 (RETURN (CDR KR1)))) (RETURN L1)))
77400 EXPR)
77500
77600 (DEFPROP S2
77700 (LAMBDA(X Y Z)
77800 (PROG (Z1)
77900 (SETQ Z1 (CDR Z))
78000 A (COND ((NULL Z1) (RETURN Z))
78100 ((VAR (CAR Z1)) (COND ((EQ (CAR Z1) Y) (RPLACA Z1 X))))
78200 ((CONST (CAR Z1)) NIL)
78300 (T (RPLACA Z1 (S2 X Y (CAR Z1)))))
78400 (SETQ Z1 (CDR Z1))
78500 (GO A)))
78600 EXPR)
78700
78800 (DEFPROP SETQUERY
78900 (LAMBDA (X) (SETQUERY2 X NIL NIL))
79000 EXPR)
79100
79200 (DEFPROP SETQUERY1
79300 (LAMBDA(XYZ XYZ1)
79400 (PROG (Z)
79500 (SETQ Z (ERRSET (SETQUERY2 XYZ XYZ1 T)))
79600 (COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (RETURN Z)))
79700 (RETURN (CONS (QUOTE NOPROOF) (CAR Z)))))
79800 EXPR)
79900
80000 (DEFPROP SETQUERY2
80100 (LAMBDA(XX YY FLG)
80200 (PROG (XYZ1
80300 CHAN
80400 Z
80500 Z1
80700 SUPPORT
80800 EDITSTRAT
80900 MERGE
81000 ORDER
81100 DEBUG
81200 DEPTH
81300 LENGTH
81400 ANCESTRY
81500 STRATEGY
81600 PMODEL
81700 NMODEL
81800 PFLG
81900 PDEPTH
82000 DLIST)
82100 (SETQ CHAN (OUTC NIL NIL))
82200 (SETQ PFLG T)
82300 (COND (FLG (UPDATESTATE YY)))
82400 (SETQ XYZ1 XX)
82500 (COND ((NULL FLG) (GO SRA1)) ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
82600 (PRINT SETQMESS)
82700 (SETQ XX (UPDATE XX))
82800 (SETQ XYZ1 XX)
82900 SRA1 (COND ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
83000 (PRINT (QUOTE HERE-ARE-THE-CLAUSES:))
83100 (SETQ N 1)
83200 AA (CLAUSES XX)
83300 SRA (COND ((AND AUTO (NULL FLG)) (SETQ Z (AUTO XYZ1)) (OUTC CHAN NIL) (RETURN Z))
83400 (AUTO (PRINT (QUOTE (STILL-AUTO (Y / N))))
83500 (COND
83600 ((EQ (READ) (QUOTE Y)) (SETQ Z (CONS XYZ1 (AUTO XYZ1))) (OUTC CHAN NIL) (RETURN Z)))))
83700 SR2A (PRINT (QUOTE THE-FOLLOWING-BUILTIN-STRATEGIES-ARE-AVAILABLE:))
83800 (PRINT
83900 (QUOTE "ANCESTRY VINE UNIT MODEL[POS ; NEG] DEFMODEL[NAME] P1 P2
84000 SUPPORT[#,..] EQUALITY[ID,#] "))
84100 (PRINT (QUOTE CHOICE-STRATEGY-IS:))
84200 (COND
84300 (FLG (OUTIT SAVESTR)
84400 (PRINT (QUOTE DO-YOU-WANT-TO-CHANGE-IT))
84500 (SETQ Z (READ))
84600 (COND ((EQ Z (QUOTE N)) (GO SRB)))))
84700 (SCANSET)
84800 (START)
84900 (SETQ Z (ERRSET (<ST>) T))
85000 (SCANRESET)
85100 (COND ((OR (NULL Z) (NULL (CAR Z))) (PRINT (QUOTE SCREWED-STRATEGY)) (GO SR2A)))
85200 (SETQ ZIN (TOP))
85300 (SETQ STRATEGY (BUILTCH ZIN))
85400 (OUTIT ZIN)
85500 (SETQ SAVESTR ZIN)
85600 SRB (SETQ DEBUG T)
85700 SRAA (PRINT (QUOTE EDIT-STRATEGY-IS:))
85800 (COND
85900 (FLG (OUTIT (CAR (LAST EDITSTRAT)))
86000 (PRINT (QUOTE DO-YOU-WANT-TO-CHANGE-IT))
86100 (SETQ Z (READ))
86200 (COND ((EQ Z (QUOTE N)) (GO SRCA)))))
86300 (SCANSET)
86400 (START)
86500 (SETQ Z1 (ERRSET (<ST>) T))
86600 (SCANRESET)
86700 (COND ((OR (NULL Z1) (NULL (CAR Z1))) (PRINT (QUOTE SCREWED-EDIT-STRATEGY)) (GO SRAA)))
86800 (SETQ ZIN (TOP))
86900 (SETQ EDITSTRAT (BUILTED ZIN))
87000 (OUTIT ZIN)
87100 SRCA (SETQ UFLG T)
87200 (SETQ Z1
87300 (LIST STRATEGY
87400 SUPPORT
87500 EDITSTRAT
87600 MERGE
87700 ORDER
87800 DEBUG
87900 DEPTH
88000 LENGTH
88100 ANCESTRY
88200 PMODEL
88300 NMODEL
88400 PFLG
88500 EQUAL
88600 PDEPTH
88700 DLIST))
88800 (OUTC CHAN NIL)
88900 (COND (FLG (RETURN (CONS XYZ1 Z1))) (T (RETURN Z1)))))
89000 EXPR)
89100
89200 (DEFPROP SETSUP
89300 (LAMBDA(X)
89400 (PROG (Z)
89500 (SETQ X (*CL X))
89600 A (COND ((NULL X) (SETQ SUPPORT Z) (RETURN NIL)))
89700 (SETQ Z (CONS (CDAR X) Z))
89800 (SETQ X (CDR X))
89900 (GO A)))
90000 EXPR)
90100
90200 (DEFPROP SUBS3TA
90300 (LAMBDA(L Z XX TS)
90400 (PROG (X1 X2 X3 Z4)
90500 (SETQ X1 (LIST (CAR Z)))
90600 (SETQ X2 X1)
90700 (GO SUB2)
90800 SUB1 (RPLACD X2 (LIST X3))
90900 (SETQ X2 (CDR X2))
91000 SUB2 (SETQ Z (CDR Z))
91100 (SETQ Z4 (CAR Z))
91200 (COND ((NULL Z) (RETURN X1))
91300 ((EQ Z XX) (SETQ X3 TS) (GO SUB1))
91400 ((VAR Z4) (SETQ X3 (SEARCH Z4 L)) (GO SUB1))
91500 ((CONST Z4) (SETQ X3 Z4) (GO SUB1))
91600 (T (SETQ X3 (SUBS3TA L Z4 XX TS)) (GO SUB1)))))
91700 EXPR)
91800
91900 (DEFPROP SUBS3T**
92000 (LAMBDA (L X) (COND ((NULL L) (SUBS3T (QUOTE ((-11 . -1))) X)) (T (SUBS3T L X))))
92100 EXPR)
92200
92300 (DEFPROP SUB*
92400 (LAMBDA(X L)
92500 (PROG (S2 Z L1)
92600 B (SETQ L1 L)
92700 A (SETQ S2 (CDADAR L1))
92800 (SETQ Z (UNI (LIST (CAR S2)) (LIST (CAAR X)) NIL))
92900 (COND (Z (RPLACA (CAR X) (CADR (SUBS3T* Z (CONS NIL (CDR S2)))))))
93000 (SETQ L1 (CDR L1))
93100 (COND (L1 (GO A)))
93200 (SETQ X (CDR X))
93300 (COND (X (GO B)))))
93400 EXPR)
93500
93600 (DEFPROP SUBSKOL
93700 (LAMBDA (C EXL) (SUBS3T EXL C))
93800 EXPR)
93900
94000 (DEFPROP SUPPORT
94100 (LAMBDA (X) (PROG NIL (COND ((NOT (EQ LVL 1)) (RETURN T)) (T (RETURN (MEMBER (CDR X) SUPPORT))))))
94200 EXPR)
94300
94400 (DEFPROP SUBSUME1
94500 (LAMBDA(C CB D DB L)
94600 (PROG (Z)
94700 SUB5 (COND ((NEG (CAR C)) (GO SUB3))
94800 ((NEG (CAR D)) (RETURN NIL))
94900 ((EQ (CAAR C) (CAAR D)) (GO SUB1))
95000 ((ORDERP (CAAR C) (CAAR D)) (RETURN NIL))
95100 (T (GO SUB2)))
95200 SUB1 (COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDAR C) (CDAR D) L))) (T (GO SUB2)))
95300 SUB4 (COND ((NULL Z) (GO SUB2)) ((NULL (CDR C)) (RETURN T)) ((SUBSUME1 (CDR C) (CDR CB) D DB Z) (RETURN T)))
95400 SUB2 (SETQ D (CDR D))
95500 (COND (D (SETQ DB (CDR DB)) (GO SUB5)))
95600 (RETURN NIL)
95700 SUB3 (COND
95800 ((NEG (CAR D))
95900 (COND ((EQ (CADAR C) (CADAR D))
96000 (COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDDAR C) (CDDAR D) L)) (GO SUB4))
96100 (T (GO SUB2))))
96200 ((ORDERP (CADAR C) (CADAR D)) (RETURN NIL))
96300 (T (GO SUB2)))))
96400 (SETQ D (CDR D))
96500 (COND (D (SETQ DB (CDR DB)) (GO SUB3)))
96600 (RETURN NIL)))
96700 EXPR)
96800
96900 (DEFPROP SUBS2T
97000 (LAMBDA(X Y Z)
97100 (PROG (U Z1)
97200 (COND ((EQ X Y) (RETURN Z)))
97300 (SETQ U (CDR Z))
97400 (GO S2)
97500 S1 (SETQ Z1 (CDAR U))
97600 (COND ((VAR Z1) (COND ((EQ Y Z1) (RPLACD (CAR U) X))))
97700 ((CONST Z1) NIL)
97800 (T (RPLACD (CAR U) (S2 X Y Z1))))
97900 (SETQ U (CDR U))
98000 S2 (COND (U (GO S1)))
98100 (RPLACD Z (CONS (CONS Y (COND ((OR (VAR X) (CONST X)) X) (T (COPY X)))) (CDR Z)))
98200 (RETURN Z)))
98300 EXPR)
98400
98500 (DEFPROP SUBS3T
98600 (LAMBDA (L X) (COND ((NEG X) (CONS ESCAPE (SUBS3T* L (CDR X)))) (T (SUBS3T* L X))))
98700 EXPR)
98800
98900 (DEFPROP SUBSUME
99000 (LAMBDA(C D)
99100 (COND ((OR (AND (ALLPOS C) (ALLNEG D)) (AND (ALLNEG C) (ALLPOS D))) NIL)
99200 ((OR (NOT (HERE C)) (NOT (HERE D))) NIL)
99300 ((NOT (GREATERP (NUM C) (NUM D))) (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))
99400 (T NIL)))
99500 EXPR)
99600
99700 (DEFPROP SUBSUME*
99800 (LAMBDA (C D) (PROG NIL (RETURN (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))))
99900 EXPR)
00100
00200 (DEFPROP SUBST1
00300 (LAMBDA(X Y Z)
00400 (COND ((ATOM Z) (COND ((EQ Y Z) X) (T Z)))
00500 ((EQUAL Y Z) X)
00600 (T (CONS (SUBST1 X Y (CAR Z)) (SUBST1 X Y (CDR Z))))))
00700 EXPR)
00800
00900 (DEFPROP TCOPY
01000 (LAMBDA (X) (COND ((NULL X) NIL) ((VAR (CAR X)) (TCOPY (CDR X))) (T (CONS X (TCOPY (CDR X))))))
01100 EXPR)
01200
01300 (DEFPROP TERMS
01400 (LAMBDA (X Y Z) (CDR (TERMS2 X Y Z)))
01500 EXPR)
01600
01700 (DEFPROP TERMS1
01800 (LAMBDA(L N)
01900 (COND ((OR (ZEROP N) (NULL L)) NIL)
02000 ((OR (VAR (CAR L)) (CONST (CAR L))) (CONS L (TERMS1 (CDR L) N)))
02100 (T (NCONC (LIST L) (TERMS1 (CDAR L) (SUB1 N)) (TERMS1 (CDR L) (SUB1 N))))))
02200 EXPR)
02300
02400 (DEFPROP TERMS2
02500 (LAMBDA(Z L N)
02600 (PROG (Z1 T1 T2)
02700 (SETQ T2 (SETQ T1 (LIST NIL)))
02800 A (COND ((NULL L) (RETURN T1))
02900 ((VAR (CAR L)) (GO B))
03000 ((CONST (CAR L)) (COND ((EQ Z (CAAR L)) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2)))) (GO B))
03100 ((EQ N 1) (GO B)))
03200 (SETQ Z1 (TERMS2 Z (CDAR L) (SUB1 N)))
03300 (COND ((EQ (CAAR L) Z) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2))))
03400 (COND ((CDR Z1) (RPLACD T2 (CDR Z1)) (SETQ T2 (LAST T2))))
03500 B (SETQ L (CDR L))
03600 (GO A)))
03700 EXPR)
03800
03900 (DEFPROP TIMEIT
04000 (LAMBDA NIL (DIFFERENCE (DIFFERENCE (TIME) (GCTIME)) TIME1))
04100 EXPR)
04200
04300 (DEFPROP TREE
04400 (LAMBDA(L)
04500 (COND ((ATOM (CDR (ANCESTOR L))) (LIST L))
04600 (T (NCONC (LIST L) (TREE (CAR (ANCESTOR L))) (TREE (CDR (ANCESTOR L)))))))
04700 EXPR)
04800
04900 (DEFPROP TREEDEP
05000 (LAMBDA(X)
05100 (PROG (Z)
05200 (SETQ Z (ANCESTOR X))
05300 (COND ((ATOM (CDR Z)) (RETURN 0)) (T (RETURN (ADD1 (MAX (TREEDEP (CAR Z)) (TREEDEP (CDR Z)))))))))
05400 EXPR)
05500
05600 (DEFPROP TRY
05700 (LAMBDA (L) (PROG (AUTO) (EVAL (CONS (QUOTE TRY1) L))))
05800 FEXPR)
05900
06000 (DEFPROP TRY1
06100 (LAMBDA(L)
06200 (PROG (FILENAM PRNO POTZTBL NEWNAME TBL TIME1 Z Z2 AXNO)
06300 (SETQ PRNO 0)
06400 T2 (COND ((NULL L) (SETQ FILENAM (QUOTE (P R F))) (GO P3)))
06500 (SETQ Z (CAR (LAST L)))
06600 (SETQ FILENAM (EXPLODE (COND ((ATOM Z) Z) (T (CAR Z)))))
06700 (EVAL (CONS (QUOTE INPUT) L))
06800 (INC T)
06900 P3 B (SETQ Z2 (INCLAUSES))
07000 (INC NIL)
07100 (COND ((NULL Z2) (RETURN NIL)))
07200 (SETQ TIME1 (DIFFERENCE (TIME) (GCTIME)))
07300 (SETQ Z2 (ATTEMPT Z2 NIL NIL))
07400 A (COND ((OR (NULL Z2) (EQ (CAR Z2) (QUOTE QED))) (RETURN (QUOTE *)))
07500 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL)))
07600 ((EQ (CAR Z2) (QUOTE ABORT))
07700 (SETQ Z2 (ATTEMPT (INITIALAX1 (APPEND (CADR Z2) (CDDR Z2))) NIL NIL))))
07800 (GO A)))
07900 FEXPR)
08000
08100 (DEFPROP TRYIT
08200 (LAMBDA NIL
08300 (PROG (Z1 Z2 R M)
08400 (SETQ CNT (ADD1 (LENGTH CLAUSES)))
08500 (SETQ EE (CDR EE))
08600 TRY3 (SETQ Z1 (CAR EE))
08700 (COND ((NOT (HERE Z1)) (GO TRY7)))
08800 (SETQ M (CHOICE Z1))
08900 (COND ((NULL M) (GO TRY7)))
09000 TRY2 (SETQ Z2 (CAR M))
09100 (COND ((NOT (HERE Z1)) (GO TRY7)) ((NOT (HERE Z2)) (GO TRY8)))
09200 TRY1 TRY1A
09300 (COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)))
09400 (SETQ R (RESOLVE Z1 Z2))
09500 (COND ((NULL R) (GO TRY6)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
09600 (SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
09700 TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY8)))
09800 (SETQ R (PARMOD Z1 Z2))
09900 (COND ((NULL R) (GO TRY8)))
10000 (SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
10100 TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
10200 (SETQ M (CDR M))
10300 (COND (M (GO TRY2)))
10400 TRY7 (SETQ EE (CDR EE))
10500 (COND ((NOT (EQ EE (CDR EE1))) (GO TRY3)))
10600 (PRINT (QUOTE COUNT))
10700 (PRINT COUNT)
10800 (PRINT (QUOTE LEVEL))
10900 (PRINT LVL)
11000 (SETQ LVL (ADD1 LVL))
11100 (PRINT (QUOTE ELAPSED-TIME))
11200 (PRINT (TIMEIT))
11300 (COND ((CDR EE1) (SETQ EE1 (LAST EE1)) (GO TRY3)))
11400 (PRINT (QUOTE NO-PROOF-FOUND))
11500 (COND (AUTO (ERR (QUOTE NOPROOF))))
11600 (UPDATE CLAUSES)
11700 (COND ((CDR EE1) (SETQ EE (CDR EE1)) (SETQ EE1 (LAST EE1)) (GO TRY3)))
11800 (ERR (QUOTE NOPROOF))))
11900 EXPR)
12000
12100 (DEFPROP TRAVERSE
12200 (LAMBDA(L)
12300 (PROG (Z Z1 Z2)
12400 (SETQ Z (ANCESTOR L))
12500 (SETQ Z1 (CAR Z))
12600 (SETQ Z (CDR Z))
12700 (COND ((NOT (ATOM (CDR (ANCESTOR Z)))) (SETQ Z2 (TRAVERSE Z))))
12800 (COND ((NOT (ATOM (CDR (ANCESTOR Z1)))) (SETQ Z2 (NCONC (TRAVERSE Z1) Z2))))
12900 (RETURN (COND ((HERE L) (CONS L Z2)) (T Z2)))))
13000 EXPR)
13100
13200 (DEFPROP UNIT
13300 (LAMBDA (X) (EQ (NUM X) 1))
13400 EXPR)
13500
13600 (DEFPROP UNITS
13700 (LAMBDA(U)
13800 (PROG (Z Z1)
13900 (COND ((NULL U) (RETURN NIL)))
14000 (SETQ Z U)
14100 UN1 (COND ((EQ (NUM (CAR Z)) 1) (SETQ Z1 (CONS (CAR Z) Z1))))
14200 (SETQ Z (CDR Z))
14300 (COND (Z (GO UN1)))
14400 (RETURN Z1)))
14500 EXPR)
14600
14700 (DEFPROP UNITRES
14800 (LAMBDA(C UP UN)
14900 (PROG (C1 Z1 U Z RES)
15000 (SETQ C1 C)
15100 (COND ((AND (ALLPOS C) (NULL UN)) (RETURN NIL)) ((AND (ALLNEG C) (NULL UP)) (RETURN NIL)))
15200 (COND ((NULL UN) (SETQ C (NEGL C)) (GO N)))
15300 (SETQ C (CDR C))
15400 B (SETQ Z1 (CAR C))
15500 (COND ((NEG Z1) (GO N)))
15600 (SETQ U UN)
15700 A (COND ((NOT (EQ (CAR Z1) (CADADR (CAR U)))) (GO A1)))
15800 (SETQ Z (UNI (CDDADR (CAR U)) (CDR Z1) NIL))
15900 (COND ((NULL Z) (GO A1)))
16000 (COND ((NULL Z) (GO A1)) ((UNIT C1) (RETURN (LIST NIL))))
16100 (SETQ RES (CONS (REDUCER C1 C) RES))
16200 (GO A2)
16300 A1 (SETQ U (CDR U))
16400 (COND (U (GO A)))
16500 A2 (SETQ C (CDR C))
16600 (COND (C (GO B)) (T (RETURN RES)))
16700 N (SETQ Z1 (CDAR C))
16800 (SETQ U UP)
16900 C (COND ((NULL U) (RETURN RES)))
17000 C2 (COND ((NOT (EQ (CAR Z1) (CAADAR U))) (GO C1)))
17100 (SETQ Z (UNI (CDADAR U) (CDR Z1) NIL))
17200 (COND ((NULL Z) (GO C1)) ((UNIT C1) (RETURN (LIST NIL))))
17300 (SETQ RES (CONS (REDUCER C1 C) RES))
17400 (GO C3)
17500 C1 (SETQ U (CDR U))
17600 (COND (U (GO C2)))
17700 C3 (SETQ C (CDR C))
17800 (COND (C (GO N)) (T (RETURN RES)))))
17900 EXPR)
18000
18100 (DEFPROP UNITREDUCT
18200 (LAMBDA(R UP UN)
18300 (PROG (Z UP1 UN1 C1 C2 RC1 RC2)
18400 (SETQ UN1 (SETQ UP1 NIL))
18500 (SETQ C1 (SETQ C2 R))
18600 A (SETQ RC1 (SETQ RC2 NIL))
18700 (COND ((NULL C2) (GO C1)) ((AND (NULL UP1) (NULL UN1)) (GO C)))
18800 B (SETQ Z (UNITRES (CAR C2) UP1 UN1))
18900 (COND ((NULL Z) (SETQ RC2 (CONS (CAR C2) RC2)))
19000 ((NULL (CAR Z)) (RETURN (LIST NIL)))
19100 (T (SETQ RC1 (APPEND Z RC1))))
19200 (SETQ C2 (CDR C2))
19300 (COND (C2 (GO B)))
19400 C1 (SETQ UP (APPEND UP1 UP))
19500 (SETQ UN (APPEND UN1 UN))
19600 C (SETQ Z (UNITRES (CAR C1) UP UN))
19700 (COND ((NULL Z) (SETQ RC2 (CONS (CAR C1) RC2)))
19800 ((NULL (CAR Z)) (RETURN (LIST NIL)))
19900 (T (SETQ RC1 (APPEND Z RC1))))
20000 (SETQ C1 (CDR C1))
20100 (COND (C1 (GO C)))
20200 (COND ((NULL RC1) (RETURN RC2)))
20300 (SETQ C2 RC2)
20400 (SETQ C1 RC1)
20500 (SETQ Z (UNITPN C1))
20600 (COND ((AND (NULL (CAR Z)) (NULL (CDR Z))) (RETURN (APPEND RC1 RC2))))
20700 (SETQ UP1 (CAR Z))
20800 (SETQ UN1 (CDR Z))
20900 (GO A)))
21000 EXPR)
21100
21200 (DEFPROP UNITPN
21300 (LAMBDA(X)
21400 (PROG (P N)
21500 A (COND
21600 ((UNIT (CAR X)) (COND ((ALLPOS (CAR X)) (SETQ P (CONS (CAR X) P))) (T (SETQ N (CONS (CAR X) N))))))
21700 (SETQ X (CDR X))
21800 (COND (X (GO A)))
21900 (RETURN (CONS P N))))
22000 EXPR)
22100
22200 (DEFPROP UNIFY
22300 (LAMBDA(X Y)
22400 (PROG (LC Z1 Z2 Z3 Z4 Z6 Z7)
22500 (SETQ LC (LIST NIL))
22600 U3 (SETQ Z1 (CAR X))
22700 (SETQ Z2 (CAR Y))
22800 (COND ((VAR Z1) (SETQ Z3 (SEARCH Z1 (CDR LC)))) (T (SETQ Z3 Z1)))
22900 (COND ((VAR Z2) (SETQ Z4 (SEARCH Z2 (CDR LC)))) (T (SETQ Z4 Z2)))
23000 (COND ((VAR Z3)
23100 (COND ((VAR Z4) (GO UN1))
23200 ((CONST Z4) (GO UN3))
23300 (T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z3 (COPY Z4)))) (GO UN2))
23400 ((NOT (VAR Z2)) (SETQ Z4 (SUBS3T* (CDR LC) Z4))))
23500 (COND ((OCCUR Z3 (CDR Z4)) (RETURN NIL)) (T (GO UN3))))))
23600 ((VAR Z4)
23700 (COND ((CONST Z3) (GO UN1))
23800 (T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z4 (COPY Z3)))) (GO UN2))
23900 ((NOT (VAR Z1)) (SETQ Z3 (SUBS3T* (CDR LC) Z3))))
24000 (COND ((OCCUR Z4 (CDR Z3)) (RETURN NIL)) (T (GO UN1))))))
24100 ((AND (CONST Z3) (CONST Z4)) (COND ((NOT (EQ (CAR Z3) (CAR Z4))) (RETURN NIL)) (T (GO UN2))))
24200 ((EQ (CAR Z3) (CAR Z4)) (SETQ Z6 (CDR (SUBS3T* (CDR LC) Z3)))
24300 (SETQ Z7 (CDR (SUBS3T* (CDR LC) Z4)))
24400 (SETQ X (APPEND Z6 (CDR X)))
24500 (SETQ Y (APPEND Z7 (CDR Y)))
24600 (GO U3))
24700 (T (RETURN NIL)))
24800 UN1 (SUBS2T Z3 Z4 LC)
24900 UN2 (SETQ X (CDR X))
25000 (COND (X (SETQ Y (CDR Y)) (GO U3)))
25100 (RETURN LC)
25200 UN3 (SUBS2T Z4 Z3 LC)
25300 (GO UN2)))
25400 EXPR)
25500
25600 (DEFPROP UNI
25700 (LAMBDA(C D L)
25800 (PROG (Z1 Z2 Z3)
25900 UN2 (SETQ Z2 (CAR D))
26000 (SETQ Z1 (SETQ Z3 (CAR C)))
26100 (COND
26200 ((VAR Z1) (SETQ Z3 (SEARCH1 Z1 L))
26300 (COND ((NULL Z3) (SETQ L (CONS (CONS Z1 Z2) L)) (GO UN1))
26400 ((VAR Z3) (COND ((EQ Z3 Z2) (GO UN1)) (T (RETURN NIL)))))))
26500 (COND ((VAR Z2) (RETURN NIL))
26600 ((CONST Z2) (COND ((EQ (CAR Z2) (CAR Z3)) (GO UN1)) (T (RETURN NIL))))
26700 ((VAR Z1) (COND ((EQUAL Z2 Z3) (GO UN1)) (T (RETURN NIL))))
26800 ((EQ (CAR Z2) (CAR Z3)) (SETQ C (APPEND (CDR Z3) (CDR C)))
26900 (SETQ D (APPEND (CDR Z2) (CDR D)))
27000 (GO UN2))
27100 (T (RETURN NIL)))
27200 UN1 (SETQ C (CDR C))
27300 (COND (C (SETQ D (CDR D)) (GO UN2)))
27400 (COND (L (RETURN L)) (T (RETURN (LIST (CONS 64 64)))))))
27500 EXPR)
27600
27700 (DEFPROP UNION
27800 (LAMBDA(Z C D YC YD)
27900 (PROG (BL L Z1 Z2 Z3 Z4 Z5 Z6 C1 C2 NEG RES M1 Z7 Z8)
28000 (SETQ NO* NO)
28100 (COND
28200 (ORDER (COND (ANCESTRY (SETQ SAT C) (SETQ L YC)) ((EQ C SAT) (SETQ L YC)) (T (SETQ L YD)))
28300 (COND ((< L (CDR SAT)) (RETURN NIL)))))
28400 (SETQ M1 0)
28500 (SETQ Z7 (ANCESTOR C))
28600 (SETQ Z8 (ANCESTOR D))
28700 (SETQ C (CDR C))
28800 (SETQ D (CDR D))
28900 (SETQ Z1 Z)
29000 (SETQ Z2 Z)
29100 (SETQ Z3 (SUBS3T** Z1 YC))
29200 (SETQ Z4 (SUBS3T** Z2 YD))
29300 UN1 (SETQ Z5 (SUBS3T** Z1 (CAR C)))
29400 (COND ((OR (EQUAL Z3 Z5) (MEMC Z5 C1)) (SETQ M1 (ADD1 M1)) (GO UN1A))
29500 ((AND (NEG Z5) (MEMC (CDR Z5) C1)) (RETURN NIL)))
29600 (SETQ C1 (CONS Z5 C1))
29700 UN1A (SETQ C (CDR C))
29800 (COND (C (GO UN1)))
29900 UN2 (SETQ Z6 (SUBS3T** Z2 (CAR D)))
30000 (COND ((AND PARRES (EQUAL Z4 Z6)) (SETQ Z6 PARRES) (GO UN2B))
30100 ((OR (EQUAL Z4 Z6) (MEMC Z6 C2)) (SETQ M1 (ADD1 M1)) (GO UN2A))
30200 ((NEG Z6) (COND ((OR (MEMC (CDR Z6) C1) (MEMC (CDR Z6) C2)) (RETURN NIL))))
30300 ((POS Z6) (COND ((MEMBER (CONS ESCAPE Z6) C1) (RETURN NIL)))))
30400 UN2B (SETQ C2 (CONS Z6 C2))
30500 UN2A (SETQ D (CDR D))
30600 (COND (D (GO UN2)))
30700 (SETQ Z2 0)
30800 (COND ((NULL C1) (COND ((NULL C2) (RETURN (LIST NIL))) (T (SETQ Z1 C2) (GO UN7))))
30900 ((NULL C2) (SETQ Z1 C1) (GO UN7)))
31000 (COND ((AND MERGE (EQ M1 2) (CDR Z7) (CDR Z8)) (RETURN NIL)))
31100 UN5 (SETQ NEG RES)
31200 (COND ((NULL C1) (SETQ Z1 C2) (GO UN7))
31300 ((NULL C2) (SETQ Z1 C1) (GO UN7))
31400 ((AND (POS (CAR C1)) (POS (CAR C2))) (GO UN3))
31500 ((AND (POS (CAR C1)) (NEG (CAR C2))) (GO UN6))
31600 ((OR (AND (NEG (CAR C1)) (POS (CAR C2))) (NOT (ORDERP (CADAR C1) (CADAR C2))))
31700 (SETQ Z1 (CAR C1))
31800 (SETQ C1 (CDR C1))
31900 (GO UN4)))
32000 UN6 (SETQ Z1 (CAR C2))
32100 (SETQ C2 (CDR C2))
32200 UN4 (UPIT Z1)
32300 (COND ((MEMBER Z1 RES) (GO UN5)) (T (SETQ Z2 (ADD1 Z2)) (SETQ RES (CONS Z1 RES)) (GO UN5)))
32400 UN7 (COND ((NULL Z1) (RETURN (LIST (CONS (LIST Z2 NEG) RES)))) ((MEMBER (CAR Z1) RES) (GO UN8)))
32500 (SETQ Z2 (ADD1 Z2))
32600 (UPIT (CAR Z1))
32700 (SETQ RES (CONS (CAR Z1) RES))
32800 (COND ((NEG (CAR Z1)) (SETQ NEG RES)))
32900 UN8 (SETQ Z1 (CDR Z1))
33000 (GO UN7)
33100 UN3 (COND ((NOT (ORDERP (CAAR C1) (CAAR C2))) (SETQ Z1 (CAR C1)) (SETQ C1 (CDR C1)) (GO UN4A)))
33200 (SETQ Z1 (CAR C2))
33300 (SETQ C2 (CDR C2))
33400 UN4A (UPIT1 (CDR Z1))
33500 (COND ((MEMBER Z1 RES) (GO UN5A)))
33600 (SETQ Z2 (ADD1 Z2))
33700 (SETQ RES (CONS Z1 RES))
33800 UN5A (COND ((NULL C1) (SETQ Z1 C2) (GO UN7)) ((NULL C2) (SETQ Z1 C1) (GO UN7)))
33900 (GO UN3)))
34000 EXPR)
34100
34200 (DEFPROP UNWIND
34300 (LAMBDA(X1 X2 Y Z N)
34400 (PROG (Z1 Z2)
34500 (SETQ Z2 (ASSOC1 X1 Z))
34600 (COND (Z2 (SETQ Z1 (CDR Z2)) (GO A)))
34700 (NCONC Y (COPYDELETED X1))
34800 (NCONC Z (LIST (CONS (LAST Y) N)))
34900 (SETQ Z1 N)
35000 (SETQ N (ADD1 N))
35100 A (SETQ Z2 (ASSOC1 X2 Z))
35200 (COND (Z2 (RETURN (CONS (CONS Z1 (CDR Z2)) N))))
35300 (NCONC Y (COPYDELETED X2))
35400 (NCONC Z (LIST (CONS (LAST Y) N)))
35500 (RETURN (CONS (CONS Z1 N) (ADD1 N)))))
35600 EXPR)
35700
35800 (DEFPROP UPDATE
35900 (LAMBDA(E)
36000 (PROG (USINGFL USING
36100 CHAN1
36200 ELOC
36300 CHAN
36400 AUTO
36500 DL1
36600 RF
36700 XYZ
36800 XYZ1
36900 CMD
37000 LOCFLG
37100 Z
37200 Z1
37300 Z2
37400 INCT
37500 Z3
37600 UEX
37700 Z1R
37800 Z2R
37900 N1
38000 R
38100 N
38200 NAME
38300 NAMELIST
38400 ZZ)
38500 (SETQ CHAN (OUTC NIL NIL))
38600 (SETQ AXNO (QUOTE INSERT))
38700 (SETQ FNNAM (QUOTE EDI))
38800 (SETQ NAMELIST (CONS (CONS (QUOTE CLAUSES) E) (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME)))
38900 (SETQ N1 (LAST NAMELIST))
39000 (SETQ INCT (INC NIL))
39100 U9 (SETQ ELOC E)
39200 (SETQ N 1)
39300 U3 (UP1A (CAR ELOC) N)
39400 U3A (TERPRI)
39500 U3AA (SETQ CMD (READ))
39600 (COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
39700 U3B(COND((NOT(ATOM CMD))(GO UER2)))
39800 U3C (SETQ CMD (EXPLODE CMD))
39900 (COND ((EQ (LENGTH CMD) 1) (GO UER1))
40000 ((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
40100 UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
40200 (GO U3A)
40300 UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
40400 (GO U3A)
40500 UDI1 (SETQ Z1 (UPGETL E NAMELIST))
40600 (COND ((NULL Z1) (GO U3A)))
40700 (CLAUSES Z1)
40800 (GO U3A)
40900 USY1 (PRINT (QUOTE THE-ENTRIES-ARE:))
41000 (SETQ Z NAMELIST)
41100 USY2 (COND ((MEMQ (CAAR Z) (QUOTE (NIL %% %INITIAL %USING))) NIL) (T (PRINT (CAAR Z))))
41200 (SETQ Z (CDR Z))
41300 (COND (Z (GO USY2)))
41400 (GO U3A)
41500 UFL2 (SETQ Z (QUOTE U))
41600 (GO UFL4)
41700 UFL3 (SETQ Z (QUOTE D))
41800 (GO UFL4)
41900 UFL1 (SETQ Z (CAR (EXPLODE (READ))))
42000 UFL4 (SETQ Z2 405104)
42100 (COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
42200 UCH1 (SETQ Z (SETQUERY1 (CONS NIL CLAUSES) STRAT))
42300 (COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (GO U3A)))
42400 (UPDATESTATE (CDDR Z))
42500 (GO U3A)
42600 UDE1 (SETQ Z2 (UPGETL E NAMELIST))
42700 (COND ((NULL Z2) (GO U3A)))
42800 (EXPUNGE Z2)
42900 (GO U3A)
43000 UIN1 (SETQ NAME (READ))
43100 (SETQ Z2 (UPGETL E NAMELIST))
43200 (COND ((NULL Z2) (GO U3A)))
43300 UIN1A
43400 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL) (T (GO USE2)))
43500 (NCONC Z1 Z2)
43600 (GO U3A)
43700 USU1 (SETQ Z1 (ERRSET (GETTERMS)))
43800 (COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
43900 ((NULL (CAR Z1)) (GO U3A)))
44000 (SETQ Z3 NIL)
44100 (SETQ Z1 (CAR Z1))
44200 USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
44300 (SETQ Z1 (CDR Z1))
44400 (COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (SETQ Z2 (SETUP Z3)) (GO UIN1A)))
44500 UUP1 (SETQ Z2 (UPGETNU))
44600 (COND ((NUMBERP Z2) (GO U8)) (T (GO U3A)))
44700 UDO1 (SETQ Z2 (UPGETNU))
44800 (COND ((NUMBERP Z2) (GO U7)) (T (GO U3A)))
44900 UAN1 (SETQ Z2 (UPGETL E NAMELIST))
45000 UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
45100 (SETQ Z2 (CDR Z2))
45200 (GO UAN2)
45300 UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
45400 (INC INCT)
45500 (OUTC CHAN NIL)
45600 (SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
45700 (SETQ Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))
45800 (RETURN (MINIMIZE (APPEND Z1 Z)))
45900 USA1 (SETQ Z2 (UPGETL E NAMELIST))
46000 (COND (Z2 (NCONC E Z2)))
46100 (GO U3A)
46200 UPA1 (SETQ Z1 (UPGETL E NAMELIST))
46300 (SETQ Z2 (UPGETL E NAMELIST))
46400 (COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
46500 USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
46600 (COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
46700 (COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
46800 (SETQ Z3 Z1)
46900 (SETQ Z DDEPTH)
47000 (SETQ DDEPTH 22)
47100 USI2 (DEMOD (LIST (CAR Z3)) Z2)
47200 (SETQ Z3 (CDR Z3))
47300 (COND (Z3 (GO USI2)))
47400 (PRINT (QUOTE CLAUSES-ARE:))
47500 (CLAUSES Z1)
47600 (SETQ DDEPTH Z)
47700 (GO U3A)
47800 UAS1 (SETQ NAME (QUOTE ASSUMPTIONS))
47900 (GO UUS3)
48000 UCU1 (QUERY)
48100 (GO U3A)
48200 UDS1 (SETQ Z1 (READ))
48300 (COND ((NOT (ATOM Z1)) (GO UDS3)))
48400 UDS2 (COND
48500 ((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
48600 (GO UDS2)))
48700 UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
48800 (GO U3A)
48900 UEO1 (OUTC CHAN1 T)
49000 (GO U3A)
49100 UUS1 (SETQ NAME (QUOTE %USING))
49200 (SETQ USINGFL T)
49300 (SETQ USING NIL)
49400 UUS3 (SETQ LOCFLG T)
49500 UUS2 (SETQ Z2 (UPGETL E NAMELIST))
49600 (SETQ USINGFL NIL)
49700 (COND ((NULL Z2) (GO U3A)))
49800 USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
49900 (COND (LOCFLG (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
50000 (T (RPLACA (CAR N1) NAME)
50100 (RPLACD (CAR N1) Z2)
50200 (RPLACD N1 (CONS (CONS NIL NIL) NIL))
50300 (SETQ N1 (CDR N1))))
50400 (GO U3A)
50500 USE1 (SETQ NAME (READ))
50600 (SETQ LOCFLG NIL)
50700 (GO UUS2)
50800 UCL1 (SETQ Z (READ))
50900 UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
51000 ((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
51100 (GO UCL2))
51200 (T (GO U3A)))
51300 UGO1 (SETQ Z1 (UPGETNU))
51400 (COND ((NOT (NUMBERP Z1)) (GO U3A)))
51500 (COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
51600 (T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
51700 UTR1 (SETQ UEX NIL)
51800 (GO UEX2)
51900 UEX1 (SETQ UEX T)
52000 UEX2 (SETQ NAME (QUOTE LEMMA))
52100 (SETQ XYZ (GETNAME (QUOTE NEGLEMMA) NAMELIST))
52200 (COND ((NULL XYZ) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
52300 (SETQ AUTO T)
52400 (SETQ Z2
52500 (ATTEMPT (INITIALAX (CONS (QUOTE THEOREM) (APPEND XYZ USING)))
52600 (COND (UEX (RESET (DLIST (GETNAME (QUOTE DLIST) NAMELIST)) (STRATEGY (SUPPORT XYZ))))
52700 (T NIL))
52800 NIL))
52900 (SETQ AUTO NIL)
53000 (GO AT1A)
53100 UST1 (STOP)
53200 (GO U3A)
53300 UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
53400 (ERR (CONS (QUOTE ABORT) (CONS Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))))
53500 U8 (COND ((EQ Z2 0) (GO U9)))
53600 U83 (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
53700 (SETQ Z2 (DIFFERENCE Z2 5))
53800 (SETQ ZZ 5)
53900 U84 (SETQ Z N)
54000 (SETQ Z3 (DIFFERENCE N ZZ))
54100 (COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
54200 (SETQ N Z3)
54300 (SETQ Z3 ELOC)
54400 (SETQ ELOC (DOWN N E))
54500 (SETQ ZZ NIL)
54600 (SETQ Z1 ELOC)
54700 U81 (COND ((EQ Z1 Z3) (GO U82)))
54800 (SETQ ZZ (CONS (CAR Z1) ZZ))
54900 (SETQ Z1 (CDR Z1))
55000 (GO U81)
55100 U82 (COND ((NULL ZZ) (GO U83)))
55200 (UP1A (CAR ZZ) (SUB1 Z))
55300 (SETQ ZZ (CDR ZZ))
55400 (SETQ Z (SUB1 Z))
55500 (GO U82)
55600 U7 (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
55700 (SETQ Z2 (PLUS Z2 N))
55800 U7A (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
55900 (SETQ ELOC (CDR ELOC))
56000 (SETQ N (ADD1 N))
56100 (UP1A (CAR ELOC) N)
56200 (COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
56300 UPR1 (TERPRI)
56400 (SETQ Z2 (UPGETL E NAMELIST))
56500 (COND ((NULL Z2) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A)))
56600 (COND ((GREATERP (LENGTH Z2) 1) (PRINT (QUOTE MORE-THAN-ONE-CLAUSE-TAKING-THE-FIRST-ONE))))
56700 (SETQ AXNO (QUOTE THEOREM))
56800 (SETQ Z3 (NEGATE (CAR Z2)))
56900 (SETQ AXNO (QUOTE INSERT))
57000 (SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
57100 (COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
57200 (SETQ NAME (QUOTE LEMMA))
57300 (SETQ LOCFLG T)
57400 (GO USE2)
57500 UME1 (SETQ Z1 (UPGETL E NAMELIST))
57600 (SETQ Z2 (UPGETL E NAMELIST))
57700 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
57800 (BAKSUB Z1 Z2)
57900 (GO U3A)
58000 UHE1 (PRINT MESSAGE)
58100 (GO U3A)
58200 URE1 (SETQ Z1 (UPGETL E NAMELIST))
58300 (SETQ Z2 (UPGETL E NAMELIST))
58400 U%RE1
58500 (SETQ RF T)
58600 URE1A
58700 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
58800 (SETQ Z1R Z1)
58900 (SETQ Z2R Z2)
59000 (SETQ Z3 NIL)
59100 (COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
59200 (COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
59300 UR3 (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
59400 ((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
59500 (COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
59600 (COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
59700 (SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
59800 UR3A (SETQ Z2R (CDR Z2R))
59900 (COND (Z2R (GO UR3)))
60000 (SETQ Z1R (CDR Z1R))
60100 (COND (Z1R (SETQ Z2R Z2) (GO UR3)))
60200 UR3B (COND ((NULL Z3)
60300 (COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
60400 (T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
60500 (RF (SETQ NAME (QUOTE RES)))
60600 (T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
60700 (SETQ Z2 Z3)
60800 (SETQ LOCFLG T)
60900 (GO AT2A)
61000 UEV1 (PRINT (QUOTE EVAL-AWAITS))
61100 (SETQ Z2 (ERRSET (EVAL (READ)) T))
61200 (COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
61300 UE2 (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
61400 (GO UEV1)
62400 AT1A (UPDATESTATE STRAT)
62500 (COND
62600 ((OR (NULL Z2) (AND (EQ (CAR Z2) (QUOTE ABORT)) (NULL (CADR Z2))))
62700 (PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
62800 (PRINC NAME)
62900 (GO U3A))
63000 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ AUTO T)
63100 (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
63200 (SETQ AUTO NIL)
63300 (GO AT1A))
63400 ((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE PROOF-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
63500 (SETQ Z2 (CADR Z2))
63600 AT2A (SETQ N 1)
63700 AT2 (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
63800 (SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
63900 (PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
64000 (PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
64100 (PRIN1 NAME)
64200 (CLAUSES Z2)
64300 (GO USE2)
64900 ))EXPR)
65000
65100 (DEFPROP UPGETL
65200 (LAMBDA(E N)
65300 (PROG (C)
65400 (SCANSET)
65500 (START)
65600 (SETQ C (ERRSET (<CLAUSES>) T))
65700 (SCANRESET)
65800 (COND ((OR (NULL C) (NULL (CAR C))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
65900 (SETQ C (TOP))
66000 (COND ((EQ C (QUOTE EMPTY)) (RETURN NIL)))
66100 (RETURN (UPGETL1 C E N))))
66200 EXPR)
66300
66400 (DEFPROP UPGETL1
66500 (LAMBDA(C E N)
66600 (PROG (N1 Z Z1 Z2 Z3 ZZ N2)
66700 AS1 (SETQ Z (CAR C))
66800 (COND ((ATOM Z)
66900 (COND ((NUMBERP Z) (SETQ N2 (QUOTE CLAUSES))
67000 (COND ((SETQ Z1 (DOWN Z E)) (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1)))))
67100 (T (RETURN NIL))))
67200 ((SETQ Z1 (GETNAME Z N)) (SETQ N2 Z) (SETQ ZZ (APPENDIT ZZ Z1)))
67300 (T (RETURN NIL))))
67400 ((EQ (CAR Z) (QUOTE STAT)) (GO AS10))
67500 ((EQ (CAR Z) (QUOTE FIND)) (GO AS20))
67600 ((EQ (CAR Z) (QUOTE DSK)) (GO AS30))
67700 ((SETQ Z1 (GETNAME (CAR Z) N)) (SETQ N2 (CAR Z)) (GO AS2))
67800 (T (RETURN NIL)))
67900 AS6 (SETQ C (CDR C))
68000 (COND (C (GO AS1)) (T (RETURN ZZ)))
68100 AS2 (SETQ Z2 (CADR Z))
68200 (SETQ N1 (CAR Z))
68300 (SETQ Z (CDR Z))
68400 (SETQ Z3 Z1)
68500 AS2A (COND ((NOT (NUMBERP Z2)) (PRINT (QUOTE NON-NUMERIC-ARG-FOR:)) (PRINC N1) (RETURN NIL)))
68600 AS3 (SETQ Z2 (SUB1 Z2))
68700 (COND ((ZEROP Z2) (GO AS4)))
68800 (SETQ Z1 (CDR Z1))
68900 (COND (Z1 (GO AS3)) (T (PRINT (QUOTE EXCEEDED-SIZE-OF:)) (PRINC N1) (RETURN NIL)))
69000 AS4 (COND
69100 ((NOT (HERE (CAR Z1))) (PRINT N1)
69200 (PRINC (QUOTE / ))
69300 (PRINC (CAR Z))
69400 (PRINC (QUOTE / ))
69500 (PRINC (QUOTE HAS-BEEN-DELETED))
69600 (RETURN NIL)))
69700 (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1))))
69800 (SETQ Z (CDR Z))
69900 (COND (Z (SETQ Z1 Z3) (SETQ Z2 (CAR Z)) (GO AS2A)))
70000 (GO AS6)
70100 AS10 (SETQ N2 (QUOTE INSERT))
70200 (SETQ ZZ (APPENDIT ZZ (SET3 (SETUP (CNF (FIXQFF (CDR Z)))))))
70300 (GO AS6)
70400 AS20 (SETQ N2 (QUOTE MATCHES))
70500 (SETQ Z (MAPIT (CADR Z) (LIST (QUOTE FUNCTION) (LIST (QUOTE LAMBDA) (QUOTE (C)) (CADDR Z))) N))
70600 (COND ((NULL Z) (GO AS6)) (T (GO AS31)))
70700 AS30 (SETQ N2 (QUOTE INPUT))
70800 (SETQ ZIN (CDR Z))
70900 (COND
71000 ((NULL (ERRSET (EVAL (LIST (QUOTE INPUT) (QUOTE DSK:) ZIN)))) (PRINT (QUOTE CONTINUING)) (GO AS6)))
71100 (INC T)
71200 (SETQ Z (INCLAUSES))
71300 (INC NIL)
71400 (COND ((NULL Z) (RETURN NIL)))
71500 AS31 (SETQ ZZ (APPENDIT ZZ Z))
71600 (GO AS6)))
71700 EXPR)
71800
71900 (DEFPROP UPGETNU
72000 (LAMBDA NIL
72100 (PROG (Z)
72200 (SETQ Z (READ))
72300 A (COND ((NUMBERP Z) (RETURN Z)))
72400 (SETQ Z (REVERSE (EXPLODE Z)))
72500 (COND ((EQ (CAR Z) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z)))) (GO A)) (T (RETURN NIL)))))
72600 EXPR)
72700
72800 (DEFPROP UPDATESTATE
72900 (LAMBDA(L)
73000 (PROG (L1)
73100 (SETQ L1 STATEVECTOR)
73200 A (COND ((NULL L) (RETURN NIL)))
73300 (SET (CAR L1) (CAR L))
73400 (SETQ L (CDR L))
73500 (SETQ L1 (CDR L1))
73600 (GO A)))
73700 EXPR)
73800
73900 (DEFPROP UPIT
74000 (LAMBDA (C) (COND ((NEG C) (UPIT1 (CDDR C))) (T (UPIT1 (CDR C)))))
74100 EXPR)
74200
74300 (DEFPROP UPIT1
74400 (LAMBDA(Z)
74500 (PROG (Z1 Z2)
74600 MAX2 (SETQ Z2 (CAR Z))
74700 (COND ((VAR Z2) (COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
74800 ((GREATERP Z2 NO*) NIL)
74900 (T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO)))
75000 (GO MAX1))
75100 ((CONST Z2) (GO MAX1))
75200 (T (UPIT1 (CDR Z2))))
75300 MAX1 (SETQ Z (CDR Z))
75400 (COND (Z (GO MAX2)))
75500 (RETURN NO)))
75600 EXPR)
75700
75800 (DEFPROP UP1A
75900 (LAMBDA(X N)
76000 (PROG NIL
76100 (TERPRI)
76200 (PRINC N)
76300 (PRINC (QUOTE / ))
76400 (COND ((HERE X) (PRFPRINT (CDR X))) (T (PRINC (QUOTE *DE*))))
76500 (RETURN NIL)))
76600 EXPR)
76700
76800 (DEFPROP UP1B
76900 (LAMBDA (X N) (PROG NIL (TERPRI) (PRINC N) (PRINC (QUOTE / )) (PRFPRINT (CDR X))))
77000 EXPR)
77100
77200 (DEFPROP VARIT
77300 (LAMBDA(Z)
77400 (PROG (Z1 Z2 BL Z3)
77500 (SETQ Z3 Z)
77600 M1 (SETQ Z2 (CAR Z))
77700 (COND ((VAR Z2)
77800 (COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
77900 (T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO))))
78000 ((EQ (CAR Z2) (QUOTE _)) (RPLACA Z (SETQ NO (ADD1 NO))))
78100 ((CONST Z2) NIL)
78200 (T (VARIT (CDR Z2))))
78300 (SETQ Z (CDR Z))
78400 (COND (Z (GO M1)))
78500 (RETURN Z3)))
78600 EXPR)
78700
78800 (DEFPROP VINE
78900 (LAMBDA (X) (NUMBERP (CDR (ANCESTOR X))))
79000 EXPR)
79100
79200 (DEFPROP <
79300 (LAMBDA(L X)
79400 (PROG (Z Z1 Z2)
79500 (SETQ Z X)
79600 (COND ((NEG L) (SETQ L (CADR L)) (SETQ Z2 T)) (T (SETQ L (CAR L))))
79700 A1 (SETQ Z1 (CAR Z))
79800 (COND ((NEG Z1) (SETQ Z1 (CADR Z1))) (T (SETQ Z1 (CAR Z1))))
79900 (COND ((NOT (ORDERP L Z1)) (GO A2))
80000 ((OR (AND (NOT Z2) (MEMBER Z1 PMODEL)) (AND Z2 (MEMBER Z1 NMODEL))) (RETURN T)))
80100 A2 (SETQ Z (CDR Z))
80200 (COND (Z (GO A1)))
80300 (RETURN NIL)))
80400 EXPR)